:: FUNCT_7 semantic presentation

theorem Th1: :: FUNCT_7:1

for b₁ being Function
for b₂ being set st rng b₁ c= b₂ holds
(id b₂) * b₁ = b₁

proof end;

theorem Th2: :: FUNCT_7:2

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₅ c= b₃ .: b₄ holds
b₃ " b₅ c= b₄

proof end;

theorem Th3: :: FUNCT_7:3

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being Element of b₁
for b₅ being Subset of b₁ st b₃ . b₄ in b₃ .: b₅ holds
b₄ in b₅

proof end;

theorem Th4: :: FUNCT_7:4

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being Element of b₁
for b₅ being Subset of b₁
for b₆ being Subset of b₂ st b₃ . b₄ in (b₃ .: b₅) \ b₆ holds
b₄ in b₅ \ (b₃ " b₆)

proof end;

theorem Th5: :: FUNCT_7:5

for b₁, b₂ being non empty set
for b₃ being Function of b₁,b₂ st b₃ is one-to-one holds
for b₄ being Element of b₂
for b₅ being Subset of b₁
for b₆ being Subset of b₂ st b₄ in (b₃ .: b₅) \ b₆ holds
(b₃ " ) . b₄ in b₅ \ (b₃ " b₆)

proof end;

theorem Th6: :: FUNCT_7:6

for b₁ being Function
for b₂ being set st b₂ in dom b₁ holds
b₁ | {b₂} = b₂ .--> (b₁ . b₂)

proof end;

registration

let c₁, c₂ be set ;
cluster a₁ .--> a₂ -> non empty ;
coherence

proof end;

end;

registration

let c₁, c₂, c₃, c₄ be set ;
cluster a₁,a₂ --> a₃,a₄ -> non empty ;
coherence

proof end;

end;

theorem Th7: :: FUNCT_7:7

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being set st b₃ in b₁ holds
b₃ .--> (b₂ . b₃) = b₂ | {b₃}

proof end;

theorem Th8: :: FUNCT_7:8

for b₁, b₂ being set
for b₃ being ManySortedSet of [:b₁,b₂:]
for b₄, b₅ being set st b₄ in b₁ & b₅ in b₂ holds
b₄,b₅ :-> (b₃ . b₄,b₅) = b₃ | [:{b₄},{b₅}:]

proof end;

theorem Th9: :: FUNCT_7:9

canceled;

theorem Th10: :: FUNCT_7:10

for b₁, b₂, b₃ being Function st rng b₂ c= dom b₁ & rng b₃ c= dom b₁ holds
b₁ * (b₂ +* b₃) = (b₁ * b₂) +* (b₁ * b₃)

proof end;

theorem Th11: :: FUNCT_7:11

for b₁, b₂, b₃ being Function holds (b₂ +* b₃) * b₁ = (b₂ * b₁) +* (b₃ * b₁)

proof end;

theorem Th12: :: FUNCT_7:12

for b₁, b₂, b₃ being Function st rng b₁ misses dom b₂ holds
(b₃ +* b₂) * b₁ = b₃ * b₁

proof end;

theorem Th13: :: FUNCT_7:13

for b₁, b₂, b₃ being set st b₁ meets rng ((id b₂) +* (b₁ --> b₃)) holds
b₃ in b₁

proof end;

theorem Th14: :: FUNCT_7:14

for b₁, b₂, b₃ being set st b₁ <> b₂ holds
not b₁ in rng ((id b₃) +* (b₁ .--> b₂))

proof end;

theorem Th15: :: FUNCT_7:15

for b₁, b₂ being set
for b₃ being Function st dom b₃ = b₁ \/ {b₂} holds
b₃ = (b₃ | b₁) +* (b₂ .--> (b₃ . b₂))

proof end;

theorem Th16: :: FUNCT_7:16

for b₁ being Function
for b₂, b₃, b₄ being set holds (b₁ +* (b₂ --> b₃)) +* (b₂ --> b₄) = b₁ +* (b₂ --> b₄)

proof end;

theorem Th17: :: FUNCT_7:17

canceled;

theorem Th18: :: FUNCT_7:18

INT <> INT *

proof end;

theorem Th19: :: FUNCT_7:19

{} * = {{} }

proof end;

theorem Th20: :: FUNCT_7:20

for b₁, b₂ being set holds
( <*b₁*> in b₂ * iff b₁ in b₂ )

proof end;

theorem Th21: :: FUNCT_7:21

for b₁, b₂ being set st b₁ * c= b₂ * holds
b₁ c= b₂

proof end;

theorem Th22: :: FUNCT_7:22

for b₁ being Subset of NAT st ( for b₂, b₃ being Nat st b₂ in b₁ & b₃ < b₂ holds
b₃ in b₁ ) holds
b₁ is Cardinal

proof end;

theorem Th23: :: FUNCT_7:23

for b₁ being finite set
for b₂ being non empty Subset-Family of b₁ ex b₃ being Element of b₂ st
for b₄ being Element of b₂ st b₄ c= b₃ holds
b₄ = b₃

proof end;

theorem Th24: :: FUNCT_7:24

for b₁, b₂ being FinSequence st len b₁ = (len b₂) + 1 holds
for b₃ being Nat holds
( b₃ in dom b₂ iff ( b₃ in dom b₁ & b₃ + 1 in dom b₁ ) )

proof end;

registration

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

proof end;

end;

registration

cluster {} -> Function-yielding ;
coherence

proof end;

let c₁ be Function;
cluster <*a₁*> -> Function-yielding ;
coherence

proof end;

let c₂ be Function;
cluster <*a₁,a₂*> -> Function-yielding ;
coherence

proof end;

let c₃ be Function;
cluster <*a₁,a₂,a₃*> -> Function-yielding ;
coherence

proof end;

end;

registration

let c₁ be Nat;
let c₂ be Function;
cluster a₁ |-> a₂ -> Function-yielding ;
coherence

proof end;

end;

registration

let c₁, c₂ be Function-yielding FinSequence;
cluster a₁ ^ a₂ -> Function-yielding ;
coherence

proof end;

end;

theorem Th25: :: FUNCT_7:25

for b₁, b₂ being FinSequence st b₁ ^ b₂ is Function-yielding holds
( b₁ is Function-yielding & b₂ is Function-yielding )

proof end;

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

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

provided

E10: for b₁ being Element of F₁()
for b₂ being Element of F₂() holds F₄(b₁,b₂) in F₃()

proof end;

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

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

provided

E10: F₁() is finite and
E11: for b₁, b₂ being Element of F₂() st F₄(b₁) = F₄(b₂) holds
b₁ = b₂

proof end;

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

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

provided

E10: for b₁ being set st b₁ in F₁() holds
ex b₂ being Element of F₂() st b₁ = F₃(b₂) and
E11: for b₁, b₂ being Element of F₂() st F₃(b₁) = F₃(b₂) holds
b₁ = b₂

proof end;

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

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

provided

E10: F₁() c= F₂() and
E11: for b₁, b₂ being Element of F₂() st F₃(b₁) = F₃(b₂) holds
b₁ = b₂

proof end;

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

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

provided

E10: P₁[ {} ] and
E11: for b₁ being Function-yielding FinSequence st P₁[b₁] holds
for b₂ being Function holds P₁[b₁ ^ <*b₂*>]

proof end;

definition

let c₁, c₂ be set ;
assume E10: c₁ in c₂ ;
func In c₁,c₂ -> Element of a₂ equals :Def1: :: FUNCT_7:def 1
a₁;
correctness by E10;

end;

:: deftheorem Def1 defines In FUNCT_7:def 1 :

theorem Th26: :: FUNCT_7:26

for b₁, b₂, b₃ being set st b₁ in b₂ /\ b₃ holds
In b₁,b₂ = In b₁,b₃

proof end;

definition

let c₁, c₂ be Function;
let c₃ be set ;
pred c₁,c₂ equal_outside c₃ means :: FUNCT_7:def 2
a₁ | ((dom a₁) \ a₃) = a₂ | ((dom a₂) \ a₃);

end;

:: deftheorem Def2 defines equal_outside FUNCT_7:def 2 :

theorem Th27: :: FUNCT_7:27

for b₁ being Function
for b₂ being set holds b₁,b₁ equal_outside b₂

proof end;

theorem Th28: :: FUNCT_7:28

for b₁, b₂ being Function
for b₃ being set st b₁,b₂ equal_outside b₃ holds
b₂,b₁ equal_outside b₃

proof end;

theorem Th29: :: FUNCT_7:29

for b₁, b₂, b₃ being Function
for b₄ being set st b₁,b₂ equal_outside b₄ & b₂,b₃ equal_outside b₄ holds
b₁,b₃ equal_outside b₄

proof end;

theorem Th30: :: FUNCT_7:30

for b₁, b₂ being Function
for b₃ being set st b₁,b₂ equal_outside b₃ holds
(dom b₁) \ b₃ = (dom b₂) \ b₃

proof end;

theorem Th31: :: FUNCT_7:31

for b₁, b₂ being Function
for b₃ being set st dom b₂ c= b₃ holds
b₁,b₁ +* b₂ equal_outside b₃

proof end;

definition

let c₁ be Function;
let c₂, c₃ be set ;
func c₁ +* c₂,c₃ -> Function equals :Def3: :: FUNCT_7:def 3
a₁ +* (a₂ .--> a₃) if a₂ in dom a₁
otherwise a₁;
correctness ;

end;

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

theorem Th32: :: FUNCT_7:32

for b₁ being Function
for b₂, b₃ being set holds dom (b₁ +* b₃,b₂) = dom b₁

proof end;

theorem Th33: :: FUNCT_7:33

for b₁ being Function
for b₂, b₃ being set st b₃ in dom b₁ holds
(b₁ +* b₃,b₂) . b₃ = b₂

proof end;

theorem Th34: :: FUNCT_7:34

for b₁ being Function
for b₂, b₃, b₄ being set st b₃ <> b₄ holds
(b₁ +* b₃,b₂) . b₄ = b₁ . b₄

proof end;

theorem Th35: :: FUNCT_7:35

for b₁ being Function
for b₂, b₃, b₄, b₅ being set st b₄ <> b₅ holds
(b₁ +* b₄,b₂) +* b₅,b₃ = (b₁ +* b₅,b₃) +* b₄,b₂

proof end;

theorem Th36: :: FUNCT_7:36

for b₁ being Function
for b₂, b₃, b₄ being set holds (b₁ +* b₄,b₂) +* b₄,b₃ = b₁ +* b₄,b₃

proof end;

theorem Th37: :: FUNCT_7:37

for b₁ being Function
for b₂ being set holds b₁ +* b₂,(b₁ . b₂) = b₁

proof end;

registration

let c₁ be FinSequence;
let c₂ be Nat;
let c₃ be set ;
cluster a₁ +* a₂,a₃ -> FinSequence-like ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be Nat;
let c₄ be Element of c₁;
redefine func +* as c₂ +* c₃,c₄ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th38: :: FUNCT_7:38

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Element of b₁
for b₄ being Nat st b₄ in dom b₂ holds
(b₂ +* b₄,b₃) /. b₄ = b₃

proof end;

theorem Th39: :: FUNCT_7:39

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Element of b₁
for b₄, b₅ being Nat st b₄ <> b₅ & b₅ in dom b₂ holds
(b₂ +* b₄,b₃) /. b₅ = b₂ /. b₅

proof end;

theorem Th40: :: FUNCT_7:40

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁
for b₅ being Nat holds b₂ +* b₅,(b₂ /. b₅) = b₂

proof end;

definition

let c₁ be set ;
let c₂ be Function-yielding FinSequence;
func compose c₂,c₁ -> Function means :Def4: :: FUNCT_7:def 4
ex b₁ being ManySortedFunction of NAT st
( a₃ = b₁ . (len a₂) & b₁ . 0 = id a₁ & ( for b₂ being Nat st b₂ + 1 in dom a₂ holds
for b₃, b₄ being Function st b₃ = b₁ . b₂ & b₄ = a₂ . (b₂ + 1) holds
b₁ . (b₂ + 1) = b₄ * b₃ ) );
uniqueness

proof end;

correctness

proof end;

end;

:: deftheorem Def4 defines compose FUNCT_7:def 4 :

definition

let c₁ be Function-yielding FinSequence;
let c₂ be set ;
func apply c₁,c₂ -> FinSequence means :Def5: :: FUNCT_7:def 5
( len a₃ = (len a₁) + 1 & a₃ . 1 = a₂ & ( for b₁ being Nat
for b₂ being Function st b₁ in dom a₁ & b₂ = a₁ . b₁ holds
a₃ . (b₁ + 1) = b₂ . (a₃ . b₁) ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def5 defines apply FUNCT_7:def 5 :

theorem Th41: :: FUNCT_7:41

for b₁ being set holds compose {} ,b₁ = id b₁

proof end;

theorem Th42: :: FUNCT_7:42

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

proof end;

theorem Th43: :: FUNCT_7:43

for b₁ being set
for b₂ being Function-yielding FinSequence
for b₃ being Function holds compose (b₂ ^ <*b₃*>),b₁ = b₃ * (compose b₂,b₁)

proof end;

theorem Th44: :: FUNCT_7:44

for b₁ being set
for b₂ being Function-yielding FinSequence
for b₃ being Function holds apply (b₂ ^ <*b₃*>),b₁ = (apply b₂,b₁) ^ <*(b₃ . ((apply b₂,b₁) . ((len b₂) + 1)))*>

proof end;

theorem Th45: :: FUNCT_7:45

for b₁ being set
for b₂ being Function-yielding FinSequence
for b₃ being Function holds compose (<*b₃*> ^ b₂),b₁ = (compose b₂,(b₃ .: b₁)) * (b₃ | b₁)

proof end;

theorem Th46: :: FUNCT_7:46

for b₁ being set
for b₂ being Function-yielding FinSequence
for b₃ being Function holds apply (<*b₃*> ^ b₂),b₁ = <*b₁*> ^ (apply b₂,(b₃ . b₁))

proof end;

theorem Th47: :: FUNCT_7:47

for b₁ being set
for b₂ being Function holds compose <*b₂*>,b₁ = b₂ * (id b₁)

proof end;

theorem Th48: :: FUNCT_7:48

for b₁ being set
for b₂ being Function st dom b₂ c= b₁ holds
compose <*b₂*>,b₁ = b₂

proof end;

theorem Th49: :: FUNCT_7:49

for b₁ being set
for b₂ being Function holds apply <*b₂*>,b₁ = <*b₁,(b₂ . b₁)*>

proof end;

theorem Th50: :: FUNCT_7:50

for b₁, b₂ being set
for b₃, b₄ being Function-yielding FinSequence st rng (compose b₃,b₁) c= b₂ holds
compose (b₃ ^ b₄),b₁ = (compose b₄,b₂) * (compose b₃,b₁)

proof end;

theorem Th51: :: FUNCT_7:51

for b₁ being set
for b₂, b₃ being Function-yielding FinSequence holds (apply (b₂ ^ b₃),b₁) . ((len (b₂ ^ b₃)) + 1) = (apply b₃,((apply b₂,b₁) . ((len b₂) + 1))) . ((len b₃) + 1)

proof end;

theorem Th52: :: FUNCT_7:52

for b₁ being set
for b₂, b₃ being Function-yielding FinSequence holds apply (b₂ ^ b₃),b₁ = (apply b₂,b₁) $^ (apply b₃,((apply b₂,b₁) . ((len b₂) + 1)))

proof end;

theorem Th53: :: FUNCT_7:53

for b₁ being set
for b₂, b₃ being Function holds compose <*b₂,b₃*>,b₁ = (b₃ * b₂) * (id b₁)

proof end;

theorem Th54: :: FUNCT_7:54

for b₁ being set
for b₂, b₃ being Function st ( dom b₂ c= b₁ or dom (b₃ * b₂) c= b₁ ) holds
compose <*b₂,b₃*>,b₁ = b₃ * b₂

proof end;

theorem Th55: :: FUNCT_7:55

for b₁ being set
for b₂, b₃ being Function holds apply <*b₂,b₃*>,b₁ = <*b₁,(b₂ . b₁),(b₃ . (b₂ . b₁))*>

proof end;

theorem Th56: :: FUNCT_7:56

for b₁ being set
for b₂, b₃, b₄ being Function holds compose <*b₂,b₃,b₄*>,b₁ = ((b₄ * b₃) * b₂) * (id b₁)

proof end;

theorem Th57: :: FUNCT_7:57

for b₁ being set
for b₂, b₃, b₄ being Function st ( dom b₂ c= b₁ or dom (b₃ * b₂) c= b₁ or dom ((b₄ * b₃) * b₂) c= b₁ ) holds
compose <*b₂,b₃,b₄*>,b₁ = (b₄ * b₃) * b₂

proof end;

theorem Th58: :: FUNCT_7:58

for b₁ being set
for b₂, b₃, b₄ being Function holds apply <*b₂,b₃,b₄*>,b₁ = <*b₁*> ^ <*(b₂ . b₁),(b₃ . (b₂ . b₁)),(b₄ . (b₃ . (b₂ . b₁)))*>

proof end;

definition

let c₁ be FinSequence;
func firstdom c₁ -> set means :Def6: :: FUNCT_7:def 6
a₂ is empty if a₁ is empty
otherwise a₂ = proj1 (a₁ . 1);
correctness ;
func lastrng c₁ -> set means :Def7: :: FUNCT_7:def 7
a₂ is empty if a₁ is empty
otherwise a₂ = proj2 (a₁ . (len a₁));
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 b₁ being Function
for b₂ being FinSequence holds
( firstdom (<*b₁*> ^ b₂) = dom b₁ & lastrng (b₂ ^ <*b₁*>) = rng b₁ )

proof end;

theorem Th61: :: FUNCT_7:61

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

proof end;

definition

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

end;

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

theorem Th62: :: FUNCT_7:62

for b₁, b₂ being FinSequence st b₁ ^ b₂ is FuncSeq-like holds
( b₁ is FuncSeq-like & b₂ 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 c₁ be Function;
cluster <*a₁*> -> 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 b₁ being set
for b₂ being FuncSequence st b₂ <> {} holds
dom (compose b₂,b₁) = (firstdom b₂) /\ b₁

proof end;

theorem Th64: :: FUNCT_7:64

for b₁ being FuncSequence holds dom (compose b₁,(firstdom b₁)) = firstdom b₁

proof end;

theorem Th65: :: FUNCT_7:65

for b₁ being FuncSequence
for b₂ being Function st rng b₂ c= firstdom b₁ holds
<*b₂*> ^ b₁ is FuncSequence

proof end;

theorem Th66: :: FUNCT_7:66

for b₁ being FuncSequence
for b₂ being Function st lastrng b₁ c= dom b₂ holds
b₁ ^ <*b₂*> is FuncSequence

proof end;

theorem Th67: :: FUNCT_7:67

for b₁, b₂ being set
for b₃ being FuncSequence st b₁ in firstdom b₃ & b₁ in b₂ holds
(apply b₃,b₁) . ((len b₃) + 1) = (compose b₃,b₂) . b₁

proof end;

definition

let c₁, c₂ be set ;
assume E37: ( c₂ is empty implies c₁ is empty ) ;
mode FuncSequence of c₁,c₂ -> FuncSequence means :Def9: :: FUNCT_7:def 9
( firstdom a₃ = a₁ & lastrng a₃ c= a₂ );
existence

proof end;

end;

:: deftheorem Def9 defines FuncSequence FUNCT_7:def 9 :

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be FuncSequence of c₂,c₁;
redefine func compose as compose c₃,c₂ -> Function of a₂,a₁;
coherence

proof end;

end;

definition

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

proof end;

end;

:: deftheorem Def10 defines FuncSequence FUNCT_7:def 10 :

registration

let c₁ be non empty non-empty FinSequence;
cluster -> non-empty FuncSeq-like FuncSequence of a₁;
coherence

proof end;

end;

theorem Th68: :: FUNCT_7:68

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

proof end;

theorem Th69: :: FUNCT_7:69

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

proof end;

Lemma40: for b₁ being set
for b₂ being Function of b₁,b₁ holds rng b₂ c= dom b₂

proof end;

Lemma41: for b₁ being Function
for b₂ being Element of NAT
for b₃, b₄ being Function of NAT , PFuncs ((dom b₁) \/ (rng b₁)),((dom b₁) \/ (rng b₁)) st b₃ . 0 = id ((dom b₁) \/ (rng b₁)) & ( for b₅ being Element of NAT ex b₆ being Function st
( b₆ = b₃ . b₅ & b₃ . (b₅ + 1) = b₆ * b₁ ) ) & b₄ . 0 = id ((dom b₁) \/ (rng b₁)) & ( for b₅ being Element of NAT ex b₆ being Function st
( b₆ = b₄ . b₅ & b₄ . (b₅ + 1) = b₆ * b₁ ) ) holds
b₃ = b₄

proof end;

definition

let c₁ be Function;
let c₂ be Element of NAT ;
func iter c₁,c₂ -> Function means :Def11: :: FUNCT_7:def 11
ex b₁ being Function of NAT , PFuncs ((dom a₁) \/ (rng a₁)),((dom a₁) \/ (rng a₁)) st
( a₃ = b₁ . a₂ & b₁ . 0 = id ((dom a₁) \/ (rng a₁)) & ( for b₂ being Element of NAT ex b₃ being Function st
( b₃ = b₁ . b₂ & b₁ . (b₂ + 1) = b₃ * a₁ ) ) );
existence

proof end;

uniqueness by Lemma41;

end;

:: deftheorem Def11 defines iter FUNCT_7:def 11 :

Lemma43: for b₁ being Function holds
( (id ((dom b₁) \/ (rng b₁))) * b₁ = b₁ & b₁ * (id ((dom b₁) \/ (rng b₁))) = b₁ )

proof end;

theorem Th70: :: FUNCT_7:70

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

proof end;

Lemma45: for b₁ being Function st rng b₁ c= dom b₁ holds
iter b₁,0 = id (dom b₁)

proof end;

theorem Th71: :: FUNCT_7:71

for b₁ being Function
for b₂ being Nat holds iter b₁,(b₂ + 1) = (iter b₁,b₂) * b₁

proof end;

theorem Th72: :: FUNCT_7:72

for b₁ being Function holds iter b₁,1 = b₁

proof end;

theorem Th73: :: FUNCT_7:73

for b₁ being Function
for b₂ being Nat holds iter b₁,(b₂ + 1) = b₁ * (iter b₁,b₂)

proof end;

theorem Th74: :: FUNCT_7:74

for b₁ being Function
for b₂ being Nat holds
( dom (iter b₁,b₂) c= (dom b₁) \/ (rng b₁) & rng (iter b₁,b₂) c= (dom b₁) \/ (rng b₁) )

proof end;

theorem Th75: :: FUNCT_7:75

for b₁ being Function
for b₂ being Nat st b₂ <> 0 holds
( dom (iter b₁,b₂) c= dom b₁ & rng (iter b₁,b₂) c= rng b₁ )

proof end;

theorem Th76: :: FUNCT_7:76

for b₁ being Function
for b₂ being Nat st rng b₁ c= dom b₁ holds
( dom (iter b₁,b₂) = dom b₁ & rng (iter b₁,b₂) c= dom b₁ )

proof end;

theorem Th77: :: FUNCT_7:77

for b₁ being Function
for b₂ being Nat holds (iter b₁,b₂) * (id ((dom b₁) \/ (rng b₁))) = iter b₁,b₂

proof end;

theorem Th78: :: FUNCT_7:78

for b₁ being Function
for b₂ being Nat holds (id ((dom b₁) \/ (rng b₁))) * (iter b₁,b₂) = iter b₁,b₂

proof end;

theorem Th79: :: FUNCT_7:79

for b₁ being Function
for b₂, b₃ being Nat holds (iter b₁,b₂) * (iter b₁,b₃) = iter b₁,(b₂ + b₃)

proof end;

Lemma53: for b₁ being Function
for b₂, b₃ being Nat st iter (iter b₁,b₂),b₃ = iter b₁,(b₂ * b₃) holds
iter (iter b₁,b₂),(b₃ + 1) = iter b₁,(b₂ * (b₃ + 1))

proof end;

theorem Th80: :: FUNCT_7:80

for b₁ being Function
for b₂, b₃ being Nat st b₂ <> 0 holds
iter (iter b₁,b₃),b₂ = iter b₁,(b₃ * b₂)

proof end;

theorem Th81: :: FUNCT_7:81

for b₁ being Function
for b₂, b₃ being Nat st rng b₁ c= dom b₁ holds
iter (iter b₁,b₂),b₃ = iter b₁,(b₂ * b₃)

proof end;

theorem Th82: :: FUNCT_7:82

for b₁ being Nat holds iter {} ,b₁ = {}

proof end;

theorem Th83: :: FUNCT_7:83

for b₁ being set
for b₂ being Nat holds iter (id b₁),b₂ = id b₁

proof end;

theorem Th84: :: FUNCT_7:84

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

proof end;

theorem Th85: :: FUNCT_7:85

for b₁ being set
for b₂ being Nat
for b₃ being Function of b₁,b₁ holds iter b₃,b₂ is Function of b₁,b₁

proof end;

theorem Th86: :: FUNCT_7:86

for b₁ being set
for b₂ being Function of b₁,b₁ holds iter b₂,0 = id b₁

proof end;

theorem Th87: :: FUNCT_7:87

for b₁ being set
for b₂, b₃ being Nat
for b₄ being Function of b₁,b₁ holds iter (iter b₄,b₂),b₃ = iter b₄,(b₂ * b₃)

proof end;

theorem Th88: :: FUNCT_7:88

for b₁ being set
for b₂ being Nat
for b₃ being PartFunc of b₁,b₁ holds iter b₃,b₂ is PartFunc of b₁,b₁

proof end;

theorem Th89: :: FUNCT_7:89

for b₁, b₂ being set
for b₃ being Function
for b₄ being Nat st b₄ <> 0 & b₁ in b₂ & b₃ = b₂ --> b₁ holds
iter b₃,b₄ = b₃

proof end;

theorem Th90: :: FUNCT_7:90

for b₁ being Function
for b₂ being Nat holds iter b₁,b₂ = compose (b₂ |-> b₁),((dom b₁) \/ (rng b₁))

proof end;