:: FUNCT_7 semantic presentation

theorem :: FUNCT_7:1

for f being Function
for X being set st rng f c= X holds
(id X) * f = f

proof end;

theorem :: FUNCT_7:2

for X being set
for Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for B being Subset of X
for C being Subset of Y st C c= f .: B holds
f " C c= B

proof end;

theorem Th3: :: FUNCT_7:3

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for x being Element of X
for A being Subset of X st f . x in f .: A holds
x in A

proof end;

theorem Th4: :: FUNCT_7:4

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for x being Element of X
for A being Subset of X
for B being Subset of Y st f . x in (f .: A) \ B holds
x in A \ (f " B)

proof end;

theorem :: FUNCT_7:5

for X, Y being non empty set
for f being Function of X,Y st f is one-to-one holds
for y being Element of Y
for A being Subset of X
for B being Subset of Y st y in (f .: A) \ B holds
(f " ) . y in A \ (f " B)

proof end;

theorem Th6: :: FUNCT_7:6

for f being Function
for a being set st a in dom f holds
f | {a} = a .--> (f . a)

proof end;

registration

let x, y be set ;
cluster x .--> y -> non empty ;
coherence

proof end;

end;

registration

let x, y, a, b be set ;
cluster x,y --> a,b -> non empty ;
coherence

proof end;

end;

theorem Th7: :: FUNCT_7:7

for I being set
for M being ManySortedSet of I
for i being set st i in I holds
i .--> (M . i) = M | {i}

proof end;

theorem :: FUNCT_7:8

for I, J being set
for M being ManySortedSet of [:I,J:]
for i, j being set st i in I & j in J holds
i,j :-> (M . i,j) = M | [:{i},{j}:]

proof end;

theorem :: FUNCT_7:9

canceled;

theorem :: FUNCT_7:10

for f, g, h being Function st rng g c= dom f & rng h c= dom f holds
f * (g +* h) = (f * g) +* (f * h)

proof end;

theorem Th11: :: FUNCT_7:11

for f, g, h being Function holds (g +* h) * f = (g * f) +* (h * f)

proof end;

theorem :: FUNCT_7:12

for f, g, h being Function st rng f misses dom g holds
(h +* g) * f = h * f

proof end;

theorem Th13: :: FUNCT_7:13

for A, B, y being set st A meets rng ((id B) +* (A --> y)) holds
y in A

proof end;

theorem :: FUNCT_7:14

for x, y, A being set st x <> y holds
not x in rng ((id A) +* (x .--> y))

proof end;

theorem :: FUNCT_7:15

for X, a being set
for f being Function st dom f = X \/ {a} holds
f = (f | X) +* (a .--> (f . a))

proof end;

theorem :: FUNCT_7:16

for f being Function
for X, y, z being set holds (f +* (X --> y)) +* (X --> z) = f +* (X --> z)

proof end;

theorem :: FUNCT_7:17

canceled;

theorem :: FUNCT_7:18

INT <> INT *

proof end;

theorem :: FUNCT_7:19

{} * = {{} }

proof end;

theorem Th20: :: FUNCT_7:20

for x, A being set holds
( <*x*> in A * iff x in A )

proof end;

theorem :: FUNCT_7:21

for A, B being set st A * c= B * holds
A c= B

proof end;

theorem :: FUNCT_7:22

for A being Subset of NAT st ( for n, m being Nat st n in A & m < n holds
m in A ) holds
A is Cardinal

proof end;

theorem :: FUNCT_7:23

for A being finite set
for X being non empty Subset-Family of A ex C being Element of X st
for B being Element of X st B c= C holds
B = C

proof end;

theorem Th24: :: FUNCT_7:24

for p, q being FinSequence st len p = (len q) + 1 holds
for i being Nat holds
( i in dom q iff ( i in dom p & i + 1 in dom p ) )

proof end;

registration

cluster non empty non-empty Function-yielding set ;
existence

proof end;

end;

registration

cluster {} -> Function-yielding ;
coherence

proof end;

let f be Function;
cluster <*f*> -> Function-yielding ;
coherence

proof end;

let g be Function;
cluster <*f,g*> -> Function-yielding ;
coherence

proof end;

let h be Function;
cluster <*f,g,h*> -> Function-yielding ;
coherence

proof end;

end;

registration

let n be Nat;
let f be Function;
cluster n |-> f -> Function-yielding ;
coherence

proof end;

end;

registration

let p, q be Function-yielding FinSequence;
cluster p ^ q -> Function-yielding ;
coherence

proof end;

end;

theorem Th25: :: FUNCT_7:25

for p, q being FinSequence st p ^ q is Function-yielding holds
( p is Function-yielding & q is Function-yielding )

proof end;

scheme :: FUNCT_7:sch 1
Kappa2D{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( Element of F₁(), Element of F₂()) -> set } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x being Element of F₁()
for y being Element of F₂() holds f . [x,y] = F₄(x,y)

provided

A1: for x being Element of F₁()
for y being Element of F₂() holds F₄(x,y) in F₃()

proof end;

scheme :: FUNCT_7:sch 2
FinMono{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set , F₄( set ) -> set } :

{ F₃(d) where d is Element of F₂() : F₄(d) in F₁() } is finite

provided

A1: F₁() is finite and
A2: for d1, d2 being Element of F₂() st F₄(d1) = F₄(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 3
CardMono{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(),{ d where d is Element of F₂() : F₃(d) in F₁() } are_equipotent

provided

A1: for x being set st x in F₁() holds
ex d being Element of F₂() st x = F₃(d) and
A2: for d1, d2 being Element of F₂() st F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 4
CardMono'{ F₁() -> set , F₂() -> non empty set , F₃( set ) -> set } :

F₁(),{ F₃(d) where d is Element of F₂() : d in F₁() } are_equipotent

provided

A1: F₁() c= F₂() and
A2: for d1, d2 being Element of F₂() st F₃(d1) = F₃(d2) holds
d1 = d2

proof end;

scheme :: FUNCT_7:sch 5
FuncSeqInd{ P₁[ set ] } :

for p being Function-yielding FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being Function-yielding FinSequence st P₁[p] holds
for f being Function holds P₁[p ^ <*f*>]

proof end;

definition

let x, y be set ;
assume A1: x in y ;
func In x,y -> Element of y equals :Def1: :: FUNCT_7:def 1
x;
correctness by A1;

end;

:: deftheorem Def1 defines In FUNCT_7:def 1 :

theorem :: FUNCT_7:26

for x, A, B being set st x in A /\ B holds
In x,A = In x,B

proof end;

definition

let f, g be Function;
let A be set ;
pred f,g equal_outside A means :: FUNCT_7:def 2
f | ((dom f) \ A) = g | ((dom g) \ A);

end;

:: deftheorem defines equal_outside FUNCT_7:def 2 :

theorem :: FUNCT_7:27

for f being Function
for A being set holds f,f equal_outside A

proof end;

theorem :: FUNCT_7:28

for f, g being Function
for A being set st f,g equal_outside A holds
g,f equal_outside A

proof end;

theorem :: FUNCT_7:29

for f, g, h being Function
for A being set st f,g equal_outside A & g,h equal_outside A holds
f,h equal_outside A

proof end;

theorem :: FUNCT_7:30

for f, g being Function
for A being set st f,g equal_outside A holds
(dom f) \ A = (dom g) \ A

proof end;

theorem :: FUNCT_7:31

for f, g being Function
for A being set st dom g c= A holds
f,f +* g equal_outside A

proof end;

definition

let f be Function;
let i, x be set ;
func f +* i,x -> Function equals :Def3: :: FUNCT_7:def 3
f +* (i .--> x) if i in dom f
otherwise f;
correctness ;

end;

:: deftheorem Def3 defines +* FUNCT_7:def 3 :

theorem Th32: :: FUNCT_7:32

for f being Function
for d, i being set holds dom (f +* i,d) = dom f

proof end;

theorem Th33: :: FUNCT_7:33

for f being Function
for d, i being set st i in dom f holds
(f +* i,d) . i = d

proof end;

theorem Th34: :: FUNCT_7:34

for f being Function
for d, i, j being set st i <> j holds
(f +* i,d) . j = f . j

proof end;

theorem :: FUNCT_7:35

for f being Function
for d, e, i, j being set st i <> j holds
(f +* i,d) +* j,e = (f +* j,e) +* i,d

proof end;

theorem :: FUNCT_7:36

for f being Function
for d, e, i being set holds (f +* i,d) +* i,e = f +* i,e

proof end;

theorem Th37: :: FUNCT_7:37

for f being Function
for i being set holds f +* i,(f . i) = f

proof end;

registration

let f be FinSequence;
let i be Nat;
let x be set ;
cluster f +* i,x -> FinSequence-like ;
coherence

proof end;

end;

definition

let D be set ;
let f be FinSequence of D;
let i be Nat;
let d be Element of D;
:: original: +*
redefine func f +* i,d -> FinSequence of D;
coherence

proof end;

end;

theorem :: FUNCT_7:38

for D being non empty set
for f being FinSequence of D
for d being Element of D
for i being Nat st i in dom f holds
(f +* i,d) /. i = d

proof end;

theorem :: FUNCT_7:39

for D being non empty set
for f being FinSequence of D
for d being Element of D
for i, j being Nat st i <> j & j in dom f holds
(f +* i,d) /. j = f /. j

proof end;

theorem :: FUNCT_7:40

for D being non empty set
for f being FinSequence of D
for d, e being Element of D
for i being Nat holds f +* i,(f /. i) = f

proof end;

definition

let X be set ;
let p be Function-yielding FinSequence;
func compose p,X -> Function means :Def4: :: FUNCT_7:def 4
ex f being ManySortedFunction of NAT st
( it = f . (len p) & f . 0 = id X & ( for i being Nat st i + 1 in dom p holds
for g, h being Function st g = f . i & h = p . (i + 1) holds
f . (i + 1) = h * g ) );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def4 defines compose FUNCT_7:def 4 :

definition

let p be Function-yielding FinSequence;
let x be set ;
func apply p,x -> FinSequence means :Def5: :: FUNCT_7:def 5
( len it = (len p) + 1 & it . 1 = x & ( for i being Nat
for f being Function st i in dom p & f = p . i holds
it . (i + 1) = f . (it . i) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def5 defines apply FUNCT_7:def 5 :

theorem Th41: :: FUNCT_7:41

for X being set holds compose {} ,X = id X

proof end;

theorem Th42: :: FUNCT_7:42

for x being set holds apply {} ,x = <*x*>

proof end;

theorem Th43: :: FUNCT_7:43

for X being set
for p being Function-yielding FinSequence
for f being Function holds compose (p ^ <*f*>),X = f * (compose p,X)

proof end;

theorem Th44: :: FUNCT_7:44

for x being set
for p being Function-yielding FinSequence
for f being Function holds apply (p ^ <*f*>),x = (apply p,x) ^ <*(f . ((apply p,x) . ((len p) + 1)))*>

proof end;

theorem :: FUNCT_7:45

for X being set
for p being Function-yielding FinSequence
for f being Function holds compose (<*f*> ^ p),X = (compose p,(f .: X)) * (f | X)

proof end;

theorem :: FUNCT_7:46

for x being set
for p being Function-yielding FinSequence
for f being Function holds apply (<*f*> ^ p),x = <*x*> ^ (apply p,(f . x))

proof end;

theorem Th47: :: FUNCT_7:47

for X being set
for f being Function holds compose <*f*>,X = f * (id X)

proof end;

theorem :: FUNCT_7:48

for X being set
for f being Function st dom f c= X holds
compose <*f*>,X = f

proof end;

theorem Th49: :: FUNCT_7:49

for x being set
for f being Function holds apply <*f*>,x = <*x,(f . x)*>

proof end;

theorem :: FUNCT_7:50

for X, Y being set
for p, q being Function-yielding FinSequence st rng (compose p,X) c= Y holds
compose (p ^ q),X = (compose q,Y) * (compose p,X)

proof end;

theorem Th51: :: FUNCT_7:51

for x being set
for p, q being Function-yielding FinSequence holds (apply (p ^ q),x) . ((len (p ^ q)) + 1) = (apply q,((apply p,x) . ((len p) + 1))) . ((len q) + 1)

proof end;

theorem :: FUNCT_7:52

for x being set
for p, q being Function-yielding FinSequence holds apply (p ^ q),x = (apply p,x) $^ (apply q,((apply p,x) . ((len p) + 1)))

proof end;

theorem Th53: :: FUNCT_7:53

for X being set
for f, g being Function holds compose <*f,g*>,X = (g * f) * (id X)

proof end;

theorem :: FUNCT_7:54

for X being set
for f, g being Function st ( dom f c= X or dom (g * f) c= X ) holds
compose <*f,g*>,X = g * f

proof end;

theorem Th55: :: FUNCT_7:55

for x being set
for f, g being Function holds apply <*f,g*>,x = <*x,(f . x),(g . (f . x))*>

proof end;

theorem Th56: :: FUNCT_7:56

for X being set
for f, g, h being Function holds compose <*f,g,h*>,X = ((h * g) * f) * (id X)

proof end;

theorem :: FUNCT_7:57

for X being set
for f, g, h being Function st ( dom f c= X or dom (g * f) c= X or dom ((h * g) * f) c= X ) holds
compose <*f,g,h*>,X = (h * g) * f

proof end;

theorem :: FUNCT_7:58

for x being set
for f, g, h being Function holds apply <*f,g,h*>,x = <*x*> ^ <*(f . x),(g . (f . x)),(h . (g . (f . x)))*>

proof end;

definition

let F be FinSequence;
func firstdom F -> set means :Def6: :: FUNCT_7:def 6
it is empty if F is empty
otherwise it = proj1 (F . 1);
correctness ;
func lastrng F -> set means :Def7: :: FUNCT_7:def 7
it is empty if F is empty
otherwise it = proj2 (F . (len F));
correctness ;

end;

:: deftheorem Def6 defines firstdom FUNCT_7:def 6 :

:: deftheorem Def7 defines lastrng FUNCT_7:def 7 :

theorem Th59: :: FUNCT_7:59

( firstdom {} = {} & lastrng {} = {} ) by Def6, Def7;

theorem Th60: :: FUNCT_7:60

for f being Function
for p being FinSequence holds
( firstdom (<*f*> ^ p) = dom f & lastrng (p ^ <*f*>) = rng f )

proof end;

theorem Th61: :: FUNCT_7:61

for X being set
for p being Function-yielding FinSequence st p <> {} holds
rng (compose p,X) c= lastrng p

proof end;

definition

let IT be FinSequence;
attr IT is FuncSeq-like means :Def8: :: FUNCT_7:def 8
ex p being FinSequence st
( len p = (len IT) + 1 & ( for i being Nat st i in dom IT holds
IT . i in Funcs (p . i),(p . (i + 1)) ) );

end;

:: deftheorem Def8 defines FuncSeq-like FUNCT_7:def 8 :

theorem Th62: :: FUNCT_7:62

for p, q being FinSequence st p ^ q is FuncSeq-like holds
( p is FuncSeq-like & q is FuncSeq-like )

proof end;

registration

cluster FuncSeq-like -> Function-yielding set ;
coherence

proof end;

end;

registration

cluster empty -> Function-yielding FuncSeq-like set ;
coherence

proof end;

end;

registration

let f be Function;
cluster <*f*> -> Function-yielding FuncSeq-like ;
coherence

proof end;

end;

registration

cluster non empty non-empty Function-yielding FuncSeq-like set ;
existence

proof end;

end;

definition

mode FuncSequence is FuncSeq-like FinSequence;

end;

theorem Th63: :: FUNCT_7:63

for X being set
for p being FuncSequence st p <> {} holds
dom (compose p,X) = (firstdom p) /\ X

proof end;

theorem Th64: :: FUNCT_7:64

for p being FuncSequence holds dom (compose p,(firstdom p)) = firstdom p

proof end;

theorem :: FUNCT_7:65

for p being FuncSequence
for f being Function st rng f c= firstdom p holds
<*f*> ^ p is FuncSequence

proof end;

theorem :: FUNCT_7:66

for p being FuncSequence
for f being Function st lastrng p c= dom f holds
p ^ <*f*> is FuncSequence

proof end;

theorem :: FUNCT_7:67

for x, X being set
for p being FuncSequence st x in firstdom p & x in X holds
(apply p,x) . ((len p) + 1) = (compose p,X) . x

proof end;

definition

let X, Y be set ;
assume A1: ( Y is empty implies X is empty ) ;
mode FuncSequence of X,Y -> FuncSequence means :Def9: :: FUNCT_7:def 9
( firstdom it = X & lastrng it c= Y );
existence

proof end;

end;

:: deftheorem Def9 defines FuncSequence FUNCT_7:def 9 :

definition

let Y be non empty set ;
let X be set ;
let F be FuncSequence of X,Y;
:: original: compose
redefine func compose F,X -> Function of X,Y;
coherence

proof end;

end;

definition

let q be non empty non-empty FinSequence;
mode FuncSequence of q -> FinSequence means :Def10: :: FUNCT_7:def 10
( (len it) + 1 = len q & ( for i being Nat st i in dom it holds
it . i in Funcs (q . i),(q . (i + 1)) ) );
existence

proof end;

end;

:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :

registration

let q be non empty non-empty FinSequence;
cluster -> non-empty FuncSeq-like FuncSequence of q;
coherence

proof end;

end;

theorem Th68: :: FUNCT_7:68

for q being non empty non-empty FinSequence
for p being FuncSequence of q st p <> {} holds
( firstdom p = q . 1 & lastrng p c= q . (len q) )

proof end;

theorem :: FUNCT_7:69

for q being non empty non-empty FinSequence
for p being FuncSequence of q holds
( dom (compose p,(q . 1)) = q . 1 & rng (compose p,(q . 1)) c= q . (len q) )

proof end;

Lm1: for X being set
for f being Function of X,X holds rng f c= dom f

proof end;

Lm2: for f being Function
for n being Element of NAT
for p1, p2 being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st p1 . 0 = id ((dom f) \/ (rng f)) & ( for k being Element of NAT ex g being Function st
( g = p1 . k & p1 . (k + 1) = g * f ) ) & p2 . 0 = id ((dom f) \/ (rng f)) & ( for k being Element of NAT ex g being Function st
( g = p2 . k & p2 . (k + 1) = g * f ) ) holds
p1 = p2

proof end;

definition

let f be Function;
let n be Element of NAT ;
func iter f,n -> Function means :Def11: :: FUNCT_7:def 11
ex p being Function of NAT , PFuncs ((dom f) \/ (rng f)),((dom f) \/ (rng f)) st
( it = p . n & p . 0 = id ((dom f) \/ (rng f)) & ( for k being Element of NAT ex g being Function st
( g = p . k & p . (k + 1) = g * f ) ) );
existence

proof end;

uniqueness by Lm2;

end;

:: deftheorem Def11 defines iter FUNCT_7:def 11 :

Lm3: for f being Function holds
( (id ((dom f) \/ (rng f))) * f = f & f * (id ((dom f) \/ (rng f))) = f )

proof end;

theorem Th70: :: FUNCT_7:70

for f being Function holds iter f,0 = id ((dom f) \/ (rng f))

proof end;

Lm4: for f being Function st rng f c= dom f holds
iter f,0 = id (dom f)

proof end;

theorem Th71: :: FUNCT_7:71

for f being Function
for n being Nat holds iter f,(n + 1) = (iter f,n) * f

proof end;

theorem Th72: :: FUNCT_7:72

for f being Function holds iter f,1 = f

proof end;

theorem Th73: :: FUNCT_7:73

for f being Function
for n being Nat holds iter f,(n + 1) = f * (iter f,n)

proof end;

theorem Th74: :: FUNCT_7:74

for f being Function
for n being Nat holds
( dom (iter f,n) c= (dom f) \/ (rng f) & rng (iter f,n) c= (dom f) \/ (rng f) )

proof end;

theorem :: FUNCT_7:75

for f being Function
for n being Nat st n <> 0 holds
( dom (iter f,n) c= dom f & rng (iter f,n) c= rng f )

proof end;

theorem Th76: :: FUNCT_7:76

for f being Function
for n being Nat st rng f c= dom f holds
( dom (iter f,n) = dom f & rng (iter f,n) c= dom f )

proof end;

theorem Th77: :: FUNCT_7:77

for f being Function
for n being Nat holds (iter f,n) * (id ((dom f) \/ (rng f))) = iter f,n

proof end;

theorem :: FUNCT_7:78

for f being Function
for n being Nat holds (id ((dom f) \/ (rng f))) * (iter f,n) = iter f,n

proof end;

theorem Th79: :: FUNCT_7:79

for f being Function
for n, m being Nat holds (iter f,n) * (iter f,m) = iter f,(n + m)

proof end;

Lm5: for f being Function
for m, k being Nat st iter (iter f,m),k = iter f,(m * k) holds
iter (iter f,m),(k + 1) = iter f,(m * (k + 1))

proof end;

theorem :: FUNCT_7:80

for f being Function
for n, m being Nat st n <> 0 holds
iter (iter f,m),n = iter f,(m * n)

proof end;

theorem Th81: :: FUNCT_7:81

for f being Function
for m, n being Nat st rng f c= dom f holds
iter (iter f,m),n = iter f,(m * n)

proof end;

theorem :: FUNCT_7:82

for n being Nat holds iter {} ,n = {}

proof end;

theorem :: FUNCT_7:83

for X being set
for n being Nat holds iter (id X),n = id X

proof end;

theorem :: FUNCT_7:84

for f being Function st rng f misses dom f holds
iter f,2 = {}

proof end;

theorem :: FUNCT_7:85

for X being set
for n being Nat
for f being Function of X,X holds iter f,n is Function of X,X

proof end;

theorem :: FUNCT_7:86

for X being set
for f being Function of X,X holds iter f,0 = id X

proof end;

theorem :: FUNCT_7:87

for X being set
for m, n being Nat
for f being Function of X,X holds iter (iter f,m),n = iter f,(m * n)

proof end;

theorem :: FUNCT_7:88

for X being set
for n being Nat
for f being PartFunc of X,X holds iter f,n is PartFunc of X,X

proof end;

theorem :: FUNCT_7:89

for a, X being set
for f being Function
for n being Nat st n <> 0 & a in X & f = X --> a holds
iter f,n = f

proof end;

theorem :: FUNCT_7:90

for f being Function
for n being Nat holds iter f,n = compose (n |-> f),((dom f) \/ (rng f))

proof end;