:: by Christoph Schwarzweller

::

:: Received November 20, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

registration

coherence

for b_{1} being non empty addLoopStr st b_{1} is Abelian & b_{1} is right_add-cancelable holds

b_{1} is left_add-cancelable

for b_{1} being non empty addLoopStr st b_{1} is Abelian & b_{1} is left_add-cancelable holds

b_{1} is right_add-cancelable

end;
for b

b

proof end;

coherence for b

b

proof end;

registration

for b_{1} being non empty addLoopStr st b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is add-associative holds

b_{1} is right_add-cancelable
;

end;

cluster non empty right_complementable add-associative right_zeroed -> non empty right_add-cancelable for addLoopStr ;

coherence for b

b

registration

ex b_{1} being non empty doubleLoopStr st

( b_{1} is Abelian & b_{1} is add-associative & b_{1} is left_zeroed & b_{1} is right_zeroed & b_{1} is commutative & b_{1} is associative & b_{1} is add-cancelable & b_{1} is distributive & b_{1} is unital )
end;

cluster non empty add-cancelable left_zeroed distributive unital associative commutative Abelian add-associative right_zeroed for doubleLoopStr ;

existence ex b

( b

proof end;

theorem Th1: :: BINOM:1

for R being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr

for a being Element of R holds (0. R) * a = 0. R

for a being Element of R holds (0. R) * a = 0. R

proof end;

theorem Th2: :: BINOM:2

for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr

for a being Element of R holds a * (0. R) = 0. R

for a being Element of R holds a * (0. R) = 0. R

proof end;

Lm1: now :: thesis: for C, D being non empty set

for b being Element of D

for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

for b being Element of D

for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

let C, D be non empty set ; :: thesis: for b being Element of D

for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

let b be Element of D; :: thesis: for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

let F be Function of [:C,D:],D; :: thesis: ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

thus ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) ) :: thesis: verum

end;
for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

let b be Element of D; :: thesis: for F being Function of [:C,D:],D ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

let F be Function of [:C,D:],D; :: thesis: ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) )

thus ex g being Function of [:NAT,C:],D st

for a being Element of C holds

( g . (0,a) = b & ( for n being Nat holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) ) :: thesis: verum

proof

A1:
for a being Element of C ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

A28: for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ;

set h = { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ;

( f = g . a & z = f . n ) } as Relation of [:NAT,C:],D by TARSKI:def 3;

A40: for x being object st x in [:NAT,C:] holds

x in dom h

x in [:NAT,C:] ;

then dom h = [:NAT,C:] by A40, TARSKI:2;

then reconsider h = h as Function of [:NAT,C:],D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C holds

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

for a being Element of C holds

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) ) ; :: thesis: verum

end;
( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

proof

ex g being Function of C,(Funcs (NAT,D)) st
let a be Element of C; :: thesis: ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

defpred S_{1}[ Nat, Element of D, Element of D] means $3 = F . (a,$2);

A2: for n being Nat

for x being Element of D ex y being Element of D st S_{1}[n,x,y]
;

ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A2);

hence ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

end;
( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

defpred S

A2: for n being Nat

for x being Element of D ex y being Element of D st S

ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds S

hence ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

proof

then consider g being Function of C,(Funcs (NAT,D)) such that
set h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ;

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;

A22: for x being object st x in C holds

x in dom h

x in C ;

then dom h = C by A22, TARSKI:2;

then reconsider h = h as Function of C,(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ;

A3: now :: thesis: for x, y1, y2 being object st [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } holds

y1 = y2

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } holds

y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } implies y1 = y2 )

assume that

A4: [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } and

A5: [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ; :: thesis: y1 = y2

consider a1 being Element of C, l1 being Element of Funcs (NAT,D) such that

A6: [x,y1] = [a1,l1] and

A7: ex f being sequence of D st

( f = l1 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a1,(f . n)) ) ) by A4;

consider a2 being Element of C, l2 being Element of Funcs (NAT,D) such that

A8: [x,y2] = [a2,l2] and

A9: ex f being sequence of D st

( f = l2 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a2,(f . n)) ) ) by A5;

consider f1 being sequence of D such that

A10: f1 = l1 and

A11: f1 . 0 = b and

A12: for n being Nat holds f1 . (n + 1) = F . (a1,(f1 . n)) by A7;

consider f2 being sequence of D such that

A13: f2 = l2 and

A14: f2 . 0 = b and

A15: for n being Nat holds f2 . (n + 1) = F . (a2,(f2 . n)) by A9;

A16: a1 = [a1,l1] `1

.= [x,y1] `1 by A6

.= x

.= [x,y2] `1

.= [a2,l2] `1 by A8

.= a2 ;

thus y1 = [x,y1] `2

.= [a1,l1] `2 by A6

.= l1

.= l2 by A10, A13, A21, A17, FUNCT_1:2

.= [a2,l2] `2

.= [x,y2] `2 by A8

.= y2 ; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } implies y1 = y2 )

assume that

A4: [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } and

A5: [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ; :: thesis: y1 = y2

consider a1 being Element of C, l1 being Element of Funcs (NAT,D) such that

A6: [x,y1] = [a1,l1] and

A7: ex f being sequence of D st

( f = l1 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a1,(f . n)) ) ) by A4;

consider a2 being Element of C, l2 being Element of Funcs (NAT,D) such that

A8: [x,y2] = [a2,l2] and

A9: ex f being sequence of D st

( f = l2 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a2,(f . n)) ) ) by A5;

consider f1 being sequence of D such that

A10: f1 = l1 and

A11: f1 . 0 = b and

A12: for n being Nat holds f1 . (n + 1) = F . (a1,(f1 . n)) by A7;

consider f2 being sequence of D such that

A13: f2 = l2 and

A14: f2 . 0 = b and

A15: for n being Nat holds f2 . (n + 1) = F . (a2,(f2 . n)) by A9;

A16: a1 = [a1,l1] `1

.= [x,y1] `1 by A6

.= x

.= [x,y2] `1

.= [a2,l2] `1 by A8

.= a2 ;

A17: now :: thesis: for x being object st x in NAT holds

f1 . x = f2 . x

A21:
( NAT = dom f1 & NAT = dom f2 )
by FUNCT_2:def 1;f1 . x = f2 . x

defpred S_{1}[ Nat] means f1 . $1 = f2 . $1;

let x be object ; :: thesis: ( x in NAT implies f1 . x = f2 . x )

assume x in NAT ; :: thesis: f1 . x = f2 . x

then reconsider x9 = x as Element of NAT ;

_{1}[ 0 ]
by A11, A14;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A20, A18);

hence f1 . x = f2 . x9

.= f2 . x ;

:: thesis: verum

end;
let x be object ; :: thesis: ( x in NAT implies f1 . x = f2 . x )

assume x in NAT ; :: thesis: f1 . x = f2 . x

then reconsider x9 = x as Element of NAT ;

A18: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A20:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A19: S_{1}[n]
; :: thesis: S_{1}[n + 1]

f1 . (n + 1) = F . (a2,(f1 . n)) by A12, A16

.= f2 . (n + 1) by A15, A19 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;
assume A19: S

f1 . (n + 1) = F . (a2,(f1 . n)) by A12, A16

.= f2 . (n + 1) by A15, A19 ;

hence S

for n being Nat holds S

hence f1 . x = f2 . x9

.= f2 . x ;

:: thesis: verum

thus y1 = [x,y1] `2

.= [a1,l1] `2 by A6

.= l1

.= l2 by A10, A13, A21, A17, FUNCT_1:2

.= [a2,l2] `2

.= [x,y2] `2 by A8

.= y2 ; :: thesis: verum

now :: thesis: for x being object st x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } holds

x in [:C,(Funcs (NAT,D)):]

then reconsider h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st ( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } holds

x in [:C,(Funcs (NAT,D)):]

let x be object ; :: thesis: ( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } implies x in [:C,(Funcs (NAT,D)):] )

assume x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ; :: thesis: x in [:C,(Funcs (NAT,D)):]

then ex a being Element of C ex l being Element of Funcs (NAT,D) st

( x = [a,l] & ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ) ;

hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } implies x in [:C,(Funcs (NAT,D)):] )

assume x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } ; :: thesis: x in [:C,(Funcs (NAT,D)):]

then ex a being Element of C ex l being Element of Funcs (NAT,D) st

( x = [a,l] & ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ) ;

hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;

A22: for x being object st x in C holds

x in dom h

proof

for x being object st x in dom h holds
let x be object ; :: thesis: ( x in C implies x in dom h )

assume A23: x in C ; :: thesis: x in dom h

then consider f being sequence of D such that

A24: ( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (x,(f . n)) ) ) by A1;

f in Funcs (NAT,D) by FUNCT_2:8;

then [x,f] in h by A23, A24;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

end;
assume A23: x in C ; :: thesis: x in dom h

then consider f being sequence of D such that

A24: ( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (x,(f . n)) ) ) by A1;

f in Funcs (NAT,D) by FUNCT_2:8;

then [x,f] in h by A23, A24;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

x in C ;

then dom h = C by A22, TARSKI:2;

then reconsider h = h as Function of C,(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

proof

hence
for a being Element of C ex f being sequence of D st
let a be Element of C; :: thesis: ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

dom h = C by FUNCT_2:def 1;

then [a,(h . a)] in h by FUNCT_1:1;

then consider a9 being Element of C, l being Element of Funcs (NAT,D) such that

A25: [a,(h . a)] = [a9,l] and

A26: ex f9 being sequence of D st

( f9 = l & f9 . 0 = b & ( for n being Nat holds f9 . (n + 1) = F . (a9,(f9 . n)) ) ) ;

A27: h . a = [a,(h . a)] `2

.= [a9,l] `2 by A25

.= l ;

a = [a,(h . a)] `1

.= [a9,l] `1 by A25

.= a9 ;

hence ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) by A26, A27; :: thesis: verum

end;
( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) )

dom h = C by FUNCT_2:def 1;

then [a,(h . a)] in h by FUNCT_1:1;

then consider a9 being Element of C, l being Element of Funcs (NAT,D) such that

A25: [a,(h . a)] = [a9,l] and

A26: ex f9 being sequence of D st

( f9 = l & f9 . 0 = b & ( for n being Nat holds f9 . (n + 1) = F . (a9,(f9 . n)) ) ) ;

A27: h . a = [a,(h . a)] `2

.= [a9,l] `2 by A25

.= l ;

a = [a,(h . a)] `1

.= [a9,l] `1 by A25

.= a9 ;

hence ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) by A26, A27; :: thesis: verum

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

A28: for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . (a,(f . n)) ) ) ;

set h = { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ;

A29: now :: thesis: for x, y1, y2 being object st [x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } & [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

y1 = y2

( f = g . a & z = f . n ) } & [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } & [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies y1 = y2 )

assume that

A30: [x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } and

A31: [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: y1 = y2

consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A32: [x,y1] = [[n1,a1],z1] and

A33: ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) by A30;

consider n2 being Element of NAT , a2 being Element of C, z2 being Element of D such that

A34: [x,y2] = [[n2,a2],z2] and

A35: ex f2 being sequence of D st

( f2 = g . a2 & z2 = f2 . n2 ) by A31;

A36: [n1,a1] = [[n1,a1],z1] `1

.= [x,y1] `1 by A32

.= x

.= [x,y2] `1

.= [[n2,a2],z2] `1 by A34

.= [n2,a2] ;

A37: a1 = [n1,a1] `2

.= [n2,a2] `2 by A36

.= a2 ;

A38: n1 = [n1,a1] `1

.= [n2,a2] `1 by A36

.= n2 ;

thus y1 = [x,y1] `2

.= [x,y2] `2 by A32, A33, A34, A35, A37, A38

.= y2 ; :: thesis: verum

end;
( f = g . a & z = f . n ) } & [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies y1 = y2 )

assume that

A30: [x,y1] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } and

A31: [x,y2] in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: y1 = y2

consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A32: [x,y1] = [[n1,a1],z1] and

A33: ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) by A30;

consider n2 being Element of NAT , a2 being Element of C, z2 being Element of D such that

A34: [x,y2] = [[n2,a2],z2] and

A35: ex f2 being sequence of D st

( f2 = g . a2 & z2 = f2 . n2 ) by A31;

A36: [n1,a1] = [[n1,a1],z1] `1

.= [x,y1] `1 by A32

.= x

.= [x,y2] `1

.= [[n2,a2],z2] `1 by A34

.= [n2,a2] ;

A37: a1 = [n1,a1] `2

.= [n2,a2] `2 by A36

.= a2 ;

A38: n1 = [n1,a1] `1

.= [n2,a2] `1 by A36

.= n2 ;

thus y1 = [x,y1] `2

.= [x,y2] `2 by A32, A33, A34, A35, A37, A38

.= y2 ; :: thesis: verum

now :: thesis: for x being object st x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

x in [:[:NAT,C:],D:]

then reconsider h = { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st ( f = g . a & z = f . n ) } holds

x in [:[:NAT,C:],D:]

let x be object ; :: thesis: ( x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies x in [:[:NAT,C:],D:] )

assume x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: x in [:[:NAT,C:],D:]

then consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A39: x = [[n1,a1],z1] and

ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) ;

[n1,a1] in [:NAT,C:] by ZFMISC_1:def 2;

hence x in [:[:NAT,C:],D:] by A39, ZFMISC_1:def 2; :: thesis: verum

end;
( f = g . a & z = f . n ) } implies x in [:[:NAT,C:],D:] )

assume x in { [[n,a],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: x in [:[:NAT,C:],D:]

then consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A39: x = [[n1,a1],z1] and

ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) ;

[n1,a1] in [:NAT,C:] by ZFMISC_1:def 2;

hence x in [:[:NAT,C:],D:] by A39, ZFMISC_1:def 2; :: thesis: verum

( f = g . a & z = f . n ) } as Relation of [:NAT,C:],D by TARSKI:def 3;

A40: for x being object st x in [:NAT,C:] holds

x in dom h

proof

for x being object st x in dom h holds
let x be object ; :: thesis: ( x in [:NAT,C:] implies x in dom h )

assume x in [:NAT,C:] ; :: thesis: x in dom h

then consider n, d being object such that

A41: n in NAT and

A42: d in C and

A43: x = [n,d] by ZFMISC_1:def 2;

reconsider d = d as Element of C by A42;

reconsider n = n as Element of NAT by A41;

consider f9 being sequence of D such that

A44: g . d = f9 and

f9 . 0 = b and

for n being Nat holds f9 . (n + 1) = F . (d,(f9 . n)) by A28;

ex z being Element of D ex f being sequence of D st

( f = g . d & z = f . n )

A45: ex f being sequence of D st

( f = g . d & z = f . n ) ;

[x,z] in h by A43, A45;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

end;
assume x in [:NAT,C:] ; :: thesis: x in dom h

then consider n, d being object such that

A41: n in NAT and

A42: d in C and

A43: x = [n,d] by ZFMISC_1:def 2;

reconsider d = d as Element of C by A42;

reconsider n = n as Element of NAT by A41;

consider f9 being sequence of D such that

A44: g . d = f9 and

f9 . 0 = b and

for n being Nat holds f9 . (n + 1) = F . (d,(f9 . n)) by A28;

ex z being Element of D ex f being sequence of D st

( f = g . d & z = f . n )

proof

then consider z being Element of D such that
take
f9 . n
; :: thesis: ex f being sequence of D st

( f = g . d & f9 . n = f . n )

take f9 ; :: thesis: ( f9 = g . d & f9 . n = f9 . n )

thus ( f9 = g . d & f9 . n = f9 . n ) by A44; :: thesis: verum

end;
( f = g . d & f9 . n = f . n )

take f9 ; :: thesis: ( f9 = g . d & f9 . n = f9 . n )

thus ( f9 = g . d & f9 . n = f9 . n ) by A44; :: thesis: verum

A45: ex f being sequence of D st

( f = g . d & z = f . n ) ;

[x,z] in h by A43, A45;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

x in [:NAT,C:] ;

then dom h = [:NAT,C:] by A40, TARSKI:2;

then reconsider h = h as Function of [:NAT,C:],D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C holds

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

for a being Element of C holds

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

proof

hence
for a being Element of C holds
let a be Element of C; :: thesis: ( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

consider f9 being sequence of D such that

A46: g . a = f9 and

A47: f9 . 0 = b and

A48: for n being Nat holds f9 . (n + 1) = F . (a,(f9 . n)) by A28;

then [0,a] in dom h by FUNCT_2:def 1;

then consider u being object such that

A63: [[0,a],u] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A64: [[0,a],u] = [[n,d],z] and

A65: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A63;

A66: u = [[0,a],u] `2

.= [[n,d],z] `2 by A64

.= z ;

A67: [0,a] = [[0,a],u] `1

.= [[n,d],z] `1 by A64

.= [n,d] ;

A68: d = [n,d] `2

.= [0,a] `2 by A67

.= a ;

n = [n,d] `1

.= [0,a] `1 by A67

.= 0 ;

hence ( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) ) by A46, A47, A63, A65, A66, A68, A49, FUNCT_1:1; :: thesis: verum

end;
consider f9 being sequence of D such that

A46: g . a = f9 and

A47: f9 . 0 = b and

A48: for n being Nat holds f9 . (n + 1) = F . (a,(f9 . n)) by A28;

A49: now :: thesis: for k being Nat holds h . ((k + 1),a) = F . (a,(h . (k,a)))

[0,a] in [:NAT,C:]
by ZFMISC_1:def 2;
let k be Nat; :: thesis: h . ((k + 1),a) = F . (a,(h . (k,a)))

[(k + 1),a] in [:NAT,C:] by ZFMISC_1:def 2;

then [(k + 1),a] in dom h by FUNCT_2:def 1;

then consider u being object such that

A50: [[(k + 1),a],u] in h by XTUPLE_0:def 12;

k in NAT by ORDINAL1:def 12;

then [k,a] in [:NAT,C:] by ZFMISC_1:def 2;

then [k,a] in dom h by FUNCT_2:def 1;

then consider v being object such that

A51: [[k,a],v] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A52: [[(k + 1),a],u] = [[n,d],z] and

A53: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A50;

A54: u = [[(k + 1),a],u] `2

.= [[n,d],z] `2 by A52

.= z ;

consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that

A55: [[k,a],v] = [[n1,d1],z1] and

A56: ex f2 being sequence of D st

( f2 = g . d1 & z1 = f2 . n1 ) by A51;

A57: v = [[k,a],v] `2

.= [[n1,d1],z1] `2 by A55

.= z1 ;

A58: [(k + 1),a] = [[(k + 1),a],u] `1

.= [[n,d],z] `1 by A52

.= [n,d] ;

A59: d = [n,d] `2

.= [(k + 1),a] `2 by A58

.= a ;

A60: [k,a] = [[k,a],v] `1

.= [[n1,d1],z1] `1 by A55

.= [n1,d1] ;

A61: n1 = [n1,d1] `1

.= [k,a] `1 by A60

.= k ;

A62: d1 = [n1,d1] `2

.= [k,a] `2 by A60

.= a ;

n = [n,d] `1

.= [(k + 1),a] `1 by A58

.= k + 1 ;

hence h . ((k + 1),a) = f9 . (k + 1) by A46, A50, A53, A54, A59, FUNCT_1:1

.= F . (a,z1) by A46, A48, A56, A61, A62

.= F . (a,(h . (k,a))) by A51, A57, FUNCT_1:1 ;

:: thesis: verum

end;
[(k + 1),a] in [:NAT,C:] by ZFMISC_1:def 2;

then [(k + 1),a] in dom h by FUNCT_2:def 1;

then consider u being object such that

A50: [[(k + 1),a],u] in h by XTUPLE_0:def 12;

k in NAT by ORDINAL1:def 12;

then [k,a] in [:NAT,C:] by ZFMISC_1:def 2;

then [k,a] in dom h by FUNCT_2:def 1;

then consider v being object such that

A51: [[k,a],v] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A52: [[(k + 1),a],u] = [[n,d],z] and

A53: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A50;

A54: u = [[(k + 1),a],u] `2

.= [[n,d],z] `2 by A52

.= z ;

consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that

A55: [[k,a],v] = [[n1,d1],z1] and

A56: ex f2 being sequence of D st

( f2 = g . d1 & z1 = f2 . n1 ) by A51;

A57: v = [[k,a],v] `2

.= [[n1,d1],z1] `2 by A55

.= z1 ;

A58: [(k + 1),a] = [[(k + 1),a],u] `1

.= [[n,d],z] `1 by A52

.= [n,d] ;

A59: d = [n,d] `2

.= [(k + 1),a] `2 by A58

.= a ;

A60: [k,a] = [[k,a],v] `1

.= [[n1,d1],z1] `1 by A55

.= [n1,d1] ;

A61: n1 = [n1,d1] `1

.= [k,a] `1 by A60

.= k ;

A62: d1 = [n1,d1] `2

.= [k,a] `2 by A60

.= a ;

n = [n,d] `1

.= [(k + 1),a] `1 by A58

.= k + 1 ;

hence h . ((k + 1),a) = f9 . (k + 1) by A46, A50, A53, A54, A59, FUNCT_1:1

.= F . (a,z1) by A46, A48, A56, A61, A62

.= F . (a,(h . (k,a))) by A51, A57, FUNCT_1:1 ;

:: thesis: verum

then [0,a] in dom h by FUNCT_2:def 1;

then consider u being object such that

A63: [[0,a],u] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A64: [[0,a],u] = [[n,d],z] and

A65: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A63;

A66: u = [[0,a],u] `2

.= [[n,d],z] `2 by A64

.= z ;

A67: [0,a] = [[0,a],u] `1

.= [[n,d],z] `1 by A64

.= [n,d] ;

A68: d = [n,d] `2

.= [0,a] `2 by A67

.= a ;

n = [n,d] `1

.= [0,a] `1 by A67

.= 0 ;

hence ( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) ) by A46, A47, A63, A65, A66, A68, A49, FUNCT_1:1; :: thesis: verum

( h . (0,a) = b & ( for n being Nat holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) ) ; :: thesis: verum

Lm2: now :: thesis: for C, D being non empty set

for b being Element of D

for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

for b being Element of D

for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

let C, D be non empty set ; :: thesis: for b being Element of D

for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

let b be Element of D; :: thesis: for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

let F be Function of [:D,C:],D; :: thesis: ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

thus ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) ) :: thesis: verum

end;
for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

let b be Element of D; :: thesis: for F being Function of [:D,C:],D ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

let F be Function of [:D,C:],D; :: thesis: ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) )

thus ex g being Function of [:C,NAT:],D st

for a being Element of C holds

( g . (a,0) = b & ( for n being Element of NAT holds g . (a,(n + 1)) = F . ((g . (a,n)),a) ) ) :: thesis: verum

proof

A1:
for a being Element of C ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

A28: for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ;

set h = { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ;

( f = g . a & z = f . n ) } as Relation of [:C,NAT:],D by TARSKI:def 3;

A40: for x being object st x in [:C,NAT:] holds

x in dom h

x in [:C,NAT:] ;

then dom h = [:C,NAT:] by A40, TARSKI:2;

then reconsider h = h as Function of [:C,NAT:],D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C holds

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )

for a being Element of C holds

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) ) ; :: thesis: verum

end;
( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

proof

ex g being Function of C,(Funcs (NAT,D)) st
let a be Element of C; :: thesis: ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

defpred S_{1}[ Nat, Element of D, Element of D] means $3 = F . ($2,a);

A2: for n being Nat

for x being Element of D ex y being Element of D st S_{1}[n,x,y]
;

ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds S_{1}[n,f . n,f . (n + 1)] ) )
from RECDEF_1:sch 2(A2);

hence ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

end;
( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

defpred S

A2: for n being Nat

for x being Element of D ex y being Element of D st S

ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds S

hence ex f being sequence of D st

( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

proof

then consider g being Function of C,(Funcs (NAT,D)) such that
set h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ;

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;

A22: for x being object st x in C holds

x in dom h

x in C ;

then dom h = C by A22, TARSKI:2;

then reconsider h = h as Function of C,(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ;

A3: now :: thesis: for x, y1, y2 being object st [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } holds

y1 = y2

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } holds

y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } implies y1 = y2 )

assume that

A4: [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } and

A5: [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ; :: thesis: y1 = y2

consider a1 being Element of C, l1 being Element of Funcs (NAT,D) such that

A6: [x,y1] = [a1,l1] and

A7: ex f being sequence of D st

( f = l1 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a1) ) ) by A4;

consider a2 being Element of C, l2 being Element of Funcs (NAT,D) such that

A8: [x,y2] = [a2,l2] and

A9: ex f being sequence of D st

( f = l2 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a2) ) ) by A5;

consider f1 being sequence of D such that

A10: f1 = l1 and

A11: f1 . 0 = b and

A12: for n being Nat holds f1 . (n + 1) = F . ((f1 . n),a1) by A7;

consider f2 being sequence of D such that

A13: f2 = l2 and

A14: f2 . 0 = b and

A15: for n being Nat holds f2 . (n + 1) = F . ((f2 . n),a2) by A9;

A16: a1 = [a1,l1] `1

.= [x,y1] `1 by A6

.= x

.= [x,y2] `1

.= [a2,l2] `1 by A8

.= a2 ;

thus y1 = [x,y1] `2

.= [a1,l1] `2 by A6

.= l1

.= l2 by A10, A13, A21, A17, FUNCT_1:2

.= [a2,l2] `2

.= [x,y2] `2 by A8

.= y2 ; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } & [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } implies y1 = y2 )

assume that

A4: [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } and

A5: [x,y2] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ; :: thesis: y1 = y2

consider a1 being Element of C, l1 being Element of Funcs (NAT,D) such that

A6: [x,y1] = [a1,l1] and

A7: ex f being sequence of D st

( f = l1 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a1) ) ) by A4;

consider a2 being Element of C, l2 being Element of Funcs (NAT,D) such that

A8: [x,y2] = [a2,l2] and

A9: ex f being sequence of D st

( f = l2 & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a2) ) ) by A5;

consider f1 being sequence of D such that

A10: f1 = l1 and

A11: f1 . 0 = b and

A12: for n being Nat holds f1 . (n + 1) = F . ((f1 . n),a1) by A7;

consider f2 being sequence of D such that

A13: f2 = l2 and

A14: f2 . 0 = b and

A15: for n being Nat holds f2 . (n + 1) = F . ((f2 . n),a2) by A9;

A16: a1 = [a1,l1] `1

.= [x,y1] `1 by A6

.= x

.= [x,y2] `1

.= [a2,l2] `1 by A8

.= a2 ;

A17: now :: thesis: for x being object st x in NAT holds

f1 . x = f2 . x

A21:
( NAT = dom f1 & NAT = dom f2 )
by FUNCT_2:def 1;f1 . x = f2 . x

defpred S_{1}[ Nat] means f1 . $1 = f2 . $1;

let x be object ; :: thesis: ( x in NAT implies f1 . x = f2 . x )

assume x in NAT ; :: thesis: f1 . x = f2 . x

then reconsider x9 = x as Element of NAT ;

_{1}[ 0 ]
by A11, A14;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A20, A18);

hence f1 . x = f2 . x9

.= f2 . x ;

:: thesis: verum

end;
let x be object ; :: thesis: ( x in NAT implies f1 . x = f2 . x )

assume x in NAT ; :: thesis: f1 . x = f2 . x

then reconsider x9 = x as Element of NAT ;

A18: now :: thesis: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

A20:
SS

let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A19: S_{1}[n]
; :: thesis: S_{1}[n + 1]

f1 . (n + 1) = F . ((f1 . n),a2) by A12, A16

.= f2 . (n + 1) by A15, A19 ;

hence S_{1}[n + 1]
; :: thesis: verum

end;
assume A19: S

f1 . (n + 1) = F . ((f1 . n),a2) by A12, A16

.= f2 . (n + 1) by A15, A19 ;

hence S

for n being Nat holds S

hence f1 . x = f2 . x9

.= f2 . x ;

:: thesis: verum

thus y1 = [x,y1] `2

.= [a1,l1] `2 by A6

.= l1

.= l2 by A10, A13, A21, A17, FUNCT_1:2

.= [a2,l2] `2

.= [x,y2] `2 by A8

.= y2 ; :: thesis: verum

now :: thesis: for x being object st x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } holds

x in [:C,(Funcs (NAT,D)):]

then reconsider h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st ( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } holds

x in [:C,(Funcs (NAT,D)):]

let x be object ; :: thesis: ( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } implies x in [:C,(Funcs (NAT,D)):] )

assume x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ; :: thesis: x in [:C,(Funcs (NAT,D)):]

then ex a being Element of C ex l being Element of Funcs (NAT,D) st

( x = [a,l] & ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ) ;

hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

end;
( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } implies x in [:C,(Funcs (NAT,D)):] )

assume x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } ; :: thesis: x in [:C,(Funcs (NAT,D)):]

then ex a being Element of C ex l being Element of Funcs (NAT,D) st

( x = [a,l] & ex f being sequence of D st

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ) ;

hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

( f = l & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;

A22: for x being object st x in C holds

x in dom h

proof

for x being object st x in dom h holds
let x be object ; :: thesis: ( x in C implies x in dom h )

assume A23: x in C ; :: thesis: x in dom h

then consider f being sequence of D such that

A24: ( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),x) ) ) by A1;

reconsider f9 = f as Element of Funcs (NAT,D) by FUNCT_2:8;

f in Funcs (NAT,D) by FUNCT_2:8;

then [x,f] in h by A23, A24;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

end;
assume A23: x in C ; :: thesis: x in dom h

then consider f being sequence of D such that

A24: ( f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),x) ) ) by A1;

reconsider f9 = f as Element of Funcs (NAT,D) by FUNCT_2:8;

f in Funcs (NAT,D) by FUNCT_2:8;

then [x,f] in h by A23, A24;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

x in C ;

then dom h = C by A22, TARSKI:2;

then reconsider h = h as Function of C,(Funcs (NAT,D)) by A3, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

for a being Element of C ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

proof

hence
for a being Element of C ex f being sequence of D st
let a be Element of C; :: thesis: ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

dom h = C by FUNCT_2:def 1;

then [a,(h . a)] in h by FUNCT_1:1;

then consider a9 being Element of C, l being Element of Funcs (NAT,D) such that

A25: [a,(h . a)] = [a9,l] and

A26: ex f9 being sequence of D st

( f9 = l & f9 . 0 = b & ( for n being Nat holds f9 . (n + 1) = F . ((f9 . n),a9) ) ) ;

A27: h . a = [a,(h . a)] `2

.= [a9,l] `2 by A25

.= l ;

a = [a,(h . a)] `1

.= [a9,l] `1 by A25

.= a9 ;

hence ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) by A26, A27; :: thesis: verum

end;
( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) )

dom h = C by FUNCT_2:def 1;

then [a,(h . a)] in h by FUNCT_1:1;

then consider a9 being Element of C, l being Element of Funcs (NAT,D) such that

A25: [a,(h . a)] = [a9,l] and

A26: ex f9 being sequence of D st

( f9 = l & f9 . 0 = b & ( for n being Nat holds f9 . (n + 1) = F . ((f9 . n),a9) ) ) ;

A27: h . a = [a,(h . a)] `2

.= [a9,l] `2 by A25

.= l ;

a = [a,(h . a)] `1

.= [a9,l] `1 by A25

.= a9 ;

hence ex f being sequence of D st

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) by A26, A27; :: thesis: verum

( h . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

A28: for a being Element of C ex f being sequence of D st

( g . a = f & f . 0 = b & ( for n being Nat holds f . (n + 1) = F . ((f . n),a) ) ) ;

set h = { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ;

A29: now :: thesis: for x, y1, y2 being object st [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

y1 = y2

( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

y1 = y2

let x, y1, y2 be object ; :: thesis: ( [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies y1 = y2 )

assume that

A30: [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } and

A31: [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: y1 = y2

consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A32: [x,y1] = [[a1,n1],z1] and

A33: ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) by A30;

consider n2 being Element of NAT , a2 being Element of C, z2 being Element of D such that

A34: [x,y2] = [[a2,n2],z2] and

A35: ex f2 being sequence of D st

( f2 = g . a2 & z2 = f2 . n2 ) by A31;

A36: [a1,n1] = [[a1,n1],z1] `1

.= [x,y1] `1 by A32

.= x

.= [x,y2] `1

.= [[a2,n2],z2] `1 by A34

.= [a2,n2] ;

A37: n1 = [a1,n1] `2

.= [a2,n2] `2 by A36

.= n2 ;

A38: a1 = [a1,n1] `1

.= [a2,n2] `1 by A36

.= a2 ;

thus y1 = [x,y1] `2

.= [x,y2] `2 by A32, A33, A34, A35, A37, A38

.= y2 ; :: thesis: verum

end;
( f = g . a & z = f . n ) } & [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies y1 = y2 )

assume that

A30: [x,y1] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } and

A31: [x,y2] in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: y1 = y2

consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A32: [x,y1] = [[a1,n1],z1] and

A33: ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) by A30;

consider n2 being Element of NAT , a2 being Element of C, z2 being Element of D such that

A34: [x,y2] = [[a2,n2],z2] and

A35: ex f2 being sequence of D st

( f2 = g . a2 & z2 = f2 . n2 ) by A31;

A36: [a1,n1] = [[a1,n1],z1] `1

.= [x,y1] `1 by A32

.= x

.= [x,y2] `1

.= [[a2,n2],z2] `1 by A34

.= [a2,n2] ;

A37: n1 = [a1,n1] `2

.= [a2,n2] `2 by A36

.= n2 ;

A38: a1 = [a1,n1] `1

.= [a2,n2] `1 by A36

.= a2 ;

thus y1 = [x,y1] `2

.= [x,y2] `2 by A32, A33, A34, A35, A37, A38

.= y2 ; :: thesis: verum

now :: thesis: for x being object st x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } holds

x in [:[:C,NAT:],D:]

then reconsider h = { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st ( f = g . a & z = f . n ) } holds

x in [:[:C,NAT:],D:]

let x be object ; :: thesis: ( x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } implies x in [:[:C,NAT:],D:] )

assume x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: x in [:[:C,NAT:],D:]

then consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A39: x = [[a1,n1],z1] and

ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) ;

[a1,n1] in [:C,NAT:] by ZFMISC_1:def 2;

hence x in [:[:C,NAT:],D:] by A39, ZFMISC_1:def 2; :: thesis: verum

end;
( f = g . a & z = f . n ) } implies x in [:[:C,NAT:],D:] )

assume x in { [[a,n],z] where n is Element of NAT , a is Element of C, z is Element of D : ex f being sequence of D st

( f = g . a & z = f . n ) } ; :: thesis: x in [:[:C,NAT:],D:]

then consider n1 being Element of NAT , a1 being Element of C, z1 being Element of D such that

A39: x = [[a1,n1],z1] and

ex f1 being sequence of D st

( f1 = g . a1 & z1 = f1 . n1 ) ;

[a1,n1] in [:C,NAT:] by ZFMISC_1:def 2;

hence x in [:[:C,NAT:],D:] by A39, ZFMISC_1:def 2; :: thesis: verum

( f = g . a & z = f . n ) } as Relation of [:C,NAT:],D by TARSKI:def 3;

A40: for x being object st x in [:C,NAT:] holds

x in dom h

proof

for x being object st x in dom h holds
let x be object ; :: thesis: ( x in [:C,NAT:] implies x in dom h )

assume x in [:C,NAT:] ; :: thesis: x in dom h

then consider d, n being object such that

A41: d in C and

A42: n in NAT and

A43: x = [d,n] by ZFMISC_1:def 2;

reconsider d = d as Element of C by A41;

reconsider n = n as Element of NAT by A42;

consider f9 being sequence of D such that

A44: g . d = f9 and

f9 . 0 = b and

for n being Nat holds f9 . (n + 1) = F . ((f9 . n),d) by A28;

ex z being Element of D ex f being sequence of D st

( f = g . d & z = f . n )

A45: ex f being sequence of D st

( f = g . d & z = f . n ) ;

[x,z] in h by A43, A45;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

end;
assume x in [:C,NAT:] ; :: thesis: x in dom h

then consider d, n being object such that

A41: d in C and

A42: n in NAT and

A43: x = [d,n] by ZFMISC_1:def 2;

reconsider d = d as Element of C by A41;

reconsider n = n as Element of NAT by A42;

consider f9 being sequence of D such that

A44: g . d = f9 and

f9 . 0 = b and

for n being Nat holds f9 . (n + 1) = F . ((f9 . n),d) by A28;

ex z being Element of D ex f being sequence of D st

( f = g . d & z = f . n )

proof

then consider z being Element of D such that
take
f9 . n
; :: thesis: ex f being sequence of D st

( f = g . d & f9 . n = f . n )

take f9 ; :: thesis: ( f9 = g . d & f9 . n = f9 . n )

thus ( f9 = g . d & f9 . n = f9 . n ) by A44; :: thesis: verum

end;
( f = g . d & f9 . n = f . n )

take f9 ; :: thesis: ( f9 = g . d & f9 . n = f9 . n )

thus ( f9 = g . d & f9 . n = f9 . n ) by A44; :: thesis: verum

A45: ex f being sequence of D st

( f = g . d & z = f . n ) ;

[x,z] in h by A43, A45;

hence x in dom h by XTUPLE_0:def 12; :: thesis: verum

x in [:C,NAT:] ;

then dom h = [:C,NAT:] by A40, TARSKI:2;

then reconsider h = h as Function of [:C,NAT:],D by A29, FUNCT_1:def 1, FUNCT_2:def 1;

take h ; :: thesis: for a being Element of C holds

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )

for a being Element of C holds

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )

proof

hence
for a being Element of C holds
let a be Element of C; :: thesis: ( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) )

consider f9 being sequence of D such that

A46: g . a = f9 and

A47: f9 . 0 = b and

A48: for n being Nat holds f9 . (n + 1) = F . ((f9 . n),a) by A28;

then [a,0] in dom h by FUNCT_2:def 1;

then consider u being object such that

A65: [[a,0],u] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A66: [[a,0],u] = [[d,n],z] and

A67: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A65;

A68: u = [[a,0],u] `2

.= [[d,n],z] `2 by A66

.= z ;

A69: [a,0] = [[a,0],u] `1

.= [[d,n],z] `1 by A66

.= [d,n] ;

A70: d = [d,n] `1

.= [a,0] `1 by A69

.= a ;

n = [d,n] `2

.= [a,0] `2 by A69

.= 0 ;

hence ( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) ) by A46, A47, A65, A67, A68, A70, A49, FUNCT_1:1; :: thesis: verum

end;
consider f9 being sequence of D such that

A46: g . a = f9 and

A47: f9 . 0 = b and

A48: for n being Nat holds f9 . (n + 1) = F . ((f9 . n),a) by A28;

A49: now :: thesis: for k being Element of NAT holds h . (a,(k + 1)) = F . ((h . (a,k)),a)

[a,0] in [:C,NAT:]
by ZFMISC_1:def 2;
let k be Element of NAT ; :: thesis: h . (a,(k + 1)) = F . ((h . (a,k)),a)

[a,(k + 1)] in [:C,NAT:] by ZFMISC_1:def 2;

then [a,(k + 1)] in dom h by FUNCT_2:def 1;

then consider u being object such that

A50: [[a,(k + 1)],u] in h by XTUPLE_0:def 12;

[a,k] in [:C,NAT:] by ZFMISC_1:def 2;

then [a,k] in dom h by FUNCT_2:def 1;

then consider v being object such that

A51: [[a,k],v] in h by XTUPLE_0:def 12;

consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that

A52: [[a,k],v] = [[d1,n1],z1] and

A53: ex f2 being sequence of D st

( f2 = g . d1 & z1 = f2 . n1 ) by A51;

A54: v = [[a,k],v] `2

.= [[d1,n1],z1] `2 by A52

.= z1 ;

A55: [a,k] = [[a,k],v] `1

.= [[d1,n1],z1] `1 by A52

.= [d1,n1] ;

A56: n1 = [d1,n1] `2

.= [a,k] `2 by A55

.= k ;

consider f2 being sequence of D such that

A57: f2 = g . d1 and

A58: z1 = f2 . n1 by A53;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A59: [[a,(k + 1)],u] = [[d,n],z] and

A60: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A50;

A61: [a,(k + 1)] = [[a,(k + 1)],u] `1

.= [[d,n],z] `1 by A59

.= [d,n] ;

A62: n = [d,n] `2

.= [a,(k + 1)] `2 by A61

.= k + 1 ;

A63: d1 = [d1,n1] `1

.= [a,k] `1 by A55

.= a ;

A64: d = [d,n] `1

.= [a,(k + 1)] `1 by A61

.= a ;

u = [[a,(k + 1)],u] `2

.= [[d,n],z] `2 by A59

.= z ;

hence h . (a,(k + 1)) = f9 . n by A46, A50, A60, A64, FUNCT_1:1

.= F . ((f2 . n1),a) by A46, A48, A62, A57, A56, A63

.= F . ((h . (a,k)),a) by A51, A58, A54, FUNCT_1:1 ;

:: thesis: verum

end;
[a,(k + 1)] in [:C,NAT:] by ZFMISC_1:def 2;

then [a,(k + 1)] in dom h by FUNCT_2:def 1;

then consider u being object such that

A50: [[a,(k + 1)],u] in h by XTUPLE_0:def 12;

[a,k] in [:C,NAT:] by ZFMISC_1:def 2;

then [a,k] in dom h by FUNCT_2:def 1;

then consider v being object such that

A51: [[a,k],v] in h by XTUPLE_0:def 12;

consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that

A52: [[a,k],v] = [[d1,n1],z1] and

A53: ex f2 being sequence of D st

( f2 = g . d1 & z1 = f2 . n1 ) by A51;

A54: v = [[a,k],v] `2

.= [[d1,n1],z1] `2 by A52

.= z1 ;

A55: [a,k] = [[a,k],v] `1

.= [[d1,n1],z1] `1 by A52

.= [d1,n1] ;

A56: n1 = [d1,n1] `2

.= [a,k] `2 by A55

.= k ;

consider f2 being sequence of D such that

A57: f2 = g . d1 and

A58: z1 = f2 . n1 by A53;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A59: [[a,(k + 1)],u] = [[d,n],z] and

A60: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A50;

A61: [a,(k + 1)] = [[a,(k + 1)],u] `1

.= [[d,n],z] `1 by A59

.= [d,n] ;

A62: n = [d,n] `2

.= [a,(k + 1)] `2 by A61

.= k + 1 ;

A63: d1 = [d1,n1] `1

.= [a,k] `1 by A55

.= a ;

A64: d = [d,n] `1

.= [a,(k + 1)] `1 by A61

.= a ;

u = [[a,(k + 1)],u] `2

.= [[d,n],z] `2 by A59

.= z ;

hence h . (a,(k + 1)) = f9 . n by A46, A50, A60, A64, FUNCT_1:1

.= F . ((f2 . n1),a) by A46, A48, A62, A57, A56, A63

.= F . ((h . (a,k)),a) by A51, A58, A54, FUNCT_1:1 ;

:: thesis: verum

then [a,0] in dom h by FUNCT_2:def 1;

then consider u being object such that

A65: [[a,0],u] in h by XTUPLE_0:def 12;

consider n being Element of NAT , d being Element of C, z being Element of D such that

A66: [[a,0],u] = [[d,n],z] and

A67: ex f1 being sequence of D st

( f1 = g . d & z = f1 . n ) by A65;

A68: u = [[a,0],u] `2

.= [[d,n],z] `2 by A66

.= z ;

A69: [a,0] = [[a,0],u] `1

.= [[d,n],z] `1 by A66

.= [d,n] ;

A70: d = [d,n] `1

.= [a,0] `1 by A69

.= a ;

n = [d,n] `2

.= [a,0] `2 by A69

.= 0 ;

hence ( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) ) by A46, A47, A65, A67, A68, A70, A49, FUNCT_1:1; :: thesis: verum

( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) ) ; :: thesis: verum

theorem :: BINOM:4

for R being non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr

for a being Element of R

for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)

for a being Element of R

for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)

proof end;

theorem Th5: :: BINOM:5

for R being non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr

for a being Element of R

for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a

for a being Element of R

for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a

proof end;

theorem :: BINOM:6

for R being non empty commutative multMagma

for a being Element of R

for p being FinSequence of the carrier of R holds p * a = a * p

for a being Element of R

for p being FinSequence of the carrier of R holds p * a = a * p

proof end;

definition

let R be non empty addLoopStr ;

let p, q be FinSequence of the carrier of R;

ex b_{1} being FinSequence of the carrier of R st

( dom b_{1} = dom p & ( for i being Nat st 1 <= i & i <= len b_{1} holds

b_{1} /. i = (p /. i) + (q /. i) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st dom b_{1} = dom p & ( for i being Nat st 1 <= i & i <= len b_{1} holds

b_{1} /. i = (p /. i) + (q /. i) ) & dom b_{2} = dom p & ( for i being Nat st 1 <= i & i <= len b_{2} holds

b_{2} /. i = (p /. i) + (q /. i) ) holds

b_{1} = b_{2}

end;
let p, q be FinSequence of the carrier of R;

func p + q -> FinSequence of the carrier of R means :Def1: :: BINOM:def 1

( dom it = dom p & ( for i being Nat st 1 <= i & i <= len it holds

it /. i = (p /. i) + (q /. i) ) );

existence ( dom it = dom p & ( for i being Nat st 1 <= i & i <= len it holds

it /. i = (p /. i) + (q /. i) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines + BINOM:def 1 :

for R being non empty addLoopStr

for p, q, b_{4} being FinSequence of the carrier of R holds

( b_{4} = p + q iff ( dom b_{4} = dom p & ( for i being Nat st 1 <= i & i <= len b_{4} holds

b_{4} /. i = (p /. i) + (q /. i) ) ) );

for R being non empty addLoopStr

for p, q, b

( b

b

theorem Th7: :: BINOM:7

for R being non empty Abelian add-associative right_zeroed addLoopStr

for p, q being FinSequence of the carrier of R st dom p = dom q holds

Sum (p + q) = (Sum p) + (Sum q)

for p, q being FinSequence of the carrier of R st dom p = dom q holds

Sum (p + q) = (Sum p) + (Sum q)

proof end;

definition

let R be non empty unital multMagma ;

let a be Element of R;

let n be Nat;

coherence

(power R) . (a,n) is Element of R ;

end;
let a be Element of R;

let n be Nat;

coherence

(power R) . (a,n) is Element of R ;

:: deftheorem defines |^ BINOM:def 2 :

for R being non empty unital multMagma

for a being Element of R

for n being Nat holds a |^ n = (power R) . (a,n);

for R being non empty unital multMagma

for a being Element of R

for n being Nat holds a |^ n = (power R) . (a,n);

theorem Th8: :: BINOM:8

for R being non empty unital multMagma

for a being Element of R holds

( a |^ 0 = 1_ R & a |^ 1 = a )

for a being Element of R holds

( a |^ 0 = 1_ R & a |^ 1 = a )

proof end;

theorem :: BINOM:9

for R being non empty unital associative commutative multMagma

for a, b being Element of R

for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)

for a, b being Element of R

for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)

proof end;

Lm3: for R being non empty unital associative multMagma

for a being Element of R

for n, m being Element of NAT holds a |^ (n + m) = (a |^ n) * (a |^ m)

proof end;

theorem Th10: :: BINOM:10

for R being non empty unital associative multMagma

for a being Element of R

for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)

for a being Element of R

for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)

proof end;

theorem :: BINOM:11

for R being non empty unital associative multMagma

for a being Element of R

for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)

for a being Element of R

for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)

proof end;

definition

let R be non empty addLoopStr ;

ex b_{1} being Function of [:NAT, the carrier of R:], the carrier of R st

for a being Element of R holds

( b_{1} . (0,a) = 0. R & ( for n being Nat holds b_{1} . ((n + 1),a) = a + (b_{1} . (n,a)) ) )

for b_{1}, b_{2} being Function of [:NAT, the carrier of R:], the carrier of R st ( for a being Element of R holds

( b_{1} . (0,a) = 0. R & ( for n being Nat holds b_{1} . ((n + 1),a) = a + (b_{1} . (n,a)) ) ) ) & ( for a being Element of R holds

( b_{2} . (0,a) = 0. R & ( for n being Nat holds b_{2} . ((n + 1),a) = a + (b_{2} . (n,a)) ) ) ) holds

b_{1} = b_{2}

ex b_{1} being Function of [: the carrier of R,NAT:], the carrier of R st

for a being Element of R holds

( b_{1} . (a,0) = 0. R & ( for n being Element of NAT holds b_{1} . (a,(n + 1)) = (b_{1} . (a,n)) + a ) )

for b_{1}, b_{2} being Function of [: the carrier of R,NAT:], the carrier of R st ( for a being Element of R holds

( b_{1} . (a,0) = 0. R & ( for n being Element of NAT holds b_{1} . (a,(n + 1)) = (b_{1} . (a,n)) + a ) ) ) & ( for a being Element of R holds

( b_{2} . (a,0) = 0. R & ( for n being Element of NAT holds b_{2} . (a,(n + 1)) = (b_{2} . (a,n)) + a ) ) ) holds

b_{1} = b_{2}

end;
func Nat-mult-left R -> Function of [:NAT, the carrier of R:], the carrier of R means :Def3: :: BINOM:def 3

for a being Element of R holds

( it . (0,a) = 0. R & ( for n being Nat holds it . ((n + 1),a) = a + (it . (n,a)) ) );

existence for a being Element of R holds

( it . (0,a) = 0. R & ( for n being Nat holds it . ((n + 1),a) = a + (it . (n,a)) ) );

ex b

for a being Element of R holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

func Nat-mult-right R -> Function of [: the carrier of R,NAT:], the carrier of R means :Def4: :: BINOM:def 4

for a being Element of R holds

( it . (a,0) = 0. R & ( for n being Element of NAT holds it . (a,(n + 1)) = (it . (a,n)) + a ) );

existence for a being Element of R holds

( it . (a,0) = 0. R & ( for n being Element of NAT holds it . (a,(n + 1)) = (it . (a,n)) + a ) );

ex b

for a being Element of R holds

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def3 defines Nat-mult-left BINOM:def 3 :

for R being non empty addLoopStr

for b_{2} being Function of [:NAT, the carrier of R:], the carrier of R holds

( b_{2} = Nat-mult-left R iff for a being Element of R holds

( b_{2} . (0,a) = 0. R & ( for n being Nat holds b_{2} . ((n + 1),a) = a + (b_{2} . (n,a)) ) ) );

for R being non empty addLoopStr

for b

( b

( b

:: deftheorem Def4 defines Nat-mult-right BINOM:def 4 :

for R being non empty addLoopStr

for b_{2} being Function of [: the carrier of R,NAT:], the carrier of R holds

( b_{2} = Nat-mult-right R iff for a being Element of R holds

( b_{2} . (a,0) = 0. R & ( for n being Element of NAT holds b_{2} . (a,(n + 1)) = (b_{2} . (a,n)) + a ) ) );

for R being non empty addLoopStr

for b

( b

( b

definition

let R be non empty addLoopStr ;

let a be Element of R;

let n be Nat;

coherence

(Nat-mult-left R) . (n,a) is Element of R ;

coherence

(Nat-mult-right R) . (a,n) is Element of R ;

end;
let a be Element of R;

let n be Nat;

coherence

(Nat-mult-left R) . (n,a) is Element of R ;

coherence

(Nat-mult-right R) . (a,n) is Element of R ;

:: deftheorem defines * BINOM:def 5 :

for R being non empty addLoopStr

for a being Element of R

for n being Nat holds n * a = (Nat-mult-left R) . (n,a);

for R being non empty addLoopStr

for a being Element of R

for n being Nat holds n * a = (Nat-mult-left R) . (n,a);

:: deftheorem defines * BINOM:def 6 :

for R being non empty addLoopStr

for a being Element of R

for n being Nat holds a * n = (Nat-mult-right R) . (a,n);

for R being non empty addLoopStr

for a being Element of R

for n being Nat holds a * n = (Nat-mult-right R) . (a,n);

theorem :: BINOM:12

theorem Th15: :: BINOM:15

for R being non empty left_zeroed add-associative addLoopStr

for a being Element of R

for n, m being Nat holds (n + m) * a = (n * a) + (m * a)

for a being Element of R

for n, m being Nat holds (n + m) * a = (n * a) + (m * a)

proof end;

theorem Th16: :: BINOM:16

for R being non empty add-associative right_zeroed addLoopStr

for a being Element of R

for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)

for a being Element of R

for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)

proof end;

theorem Th17: :: BINOM:17

for R being non empty left_zeroed add-associative right_zeroed addLoopStr

for a being Element of R

for n being Element of NAT holds n * a = a * n

for a being Element of R

for n being Element of NAT holds n * a = a * n

proof end;

theorem :: BINOM:18

for R being non empty Abelian addLoopStr

for a being Element of R

for n being Element of NAT holds n * a = a * n

for a being Element of R

for n being Element of NAT holds n * a = a * n

proof end;

theorem Th19: :: BINOM:19

for R being non empty left_add-cancelable left_zeroed left-distributive add-associative right_zeroed doubleLoopStr

for a, b being Element of R

for n being Element of NAT holds (n * a) * b = n * (a * b)

for a, b being Element of R

for n being Element of NAT holds (n * a) * b = n * (a * b)

proof end;

theorem Th20: :: BINOM:20

for R being non empty right_add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr

for a, b being Element of R

for n being Element of NAT holds b * (n * a) = (b * a) * n

for a, b being Element of R

for n being Element of NAT holds b * (n * a) = (b * a) * n

proof end;

theorem Th21: :: BINOM:21

for R being non empty add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr

for a, b being Element of R

for n being Element of NAT holds (a * n) * b = a * (n * b)

for a, b being Element of R

for n being Element of NAT holds (a * n) * b = a * (n * b)

proof end;

definition

let R be non empty unital doubleLoopStr ;

let a, b be Element of R;

let n be Nat;

ex b_{1} being FinSequence of the carrier of R st

( len b_{1} = n + 1 & ( for i, l, m being Nat st i in dom b_{1} & m = i - 1 & l = n - m holds

b_{1} /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )

for b_{1}, b_{2} being FinSequence of the carrier of R st len b_{1} = n + 1 & ( for i, l, m being Nat st i in dom b_{1} & m = i - 1 & l = n - m holds

b_{1} /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b_{2} = n + 1 & ( for i, l, m being Nat st i in dom b_{2} & m = i - 1 & l = n - m holds

b_{2} /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds

b_{1} = b_{2}

end;
let a, b be Element of R;

let n be Nat;

func (a,b) In_Power n -> FinSequence of the carrier of R means :Def7: :: BINOM:def 7

( len it = n + 1 & ( for i, l, m being Nat st i in dom it & m = i - 1 & l = n - m holds

it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );

existence ( len it = n + 1 & ( for i, l, m being Nat st i in dom it & m = i - 1 & l = n - m holds

it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );

ex b

( len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def7 defines In_Power BINOM:def 7 :

for R being non empty unital doubleLoopStr

for a, b being Element of R

for n being Nat

for b_{5} being FinSequence of the carrier of R holds

( b_{5} = (a,b) In_Power n iff ( len b_{5} = n + 1 & ( for i, l, m being Nat st i in dom b_{5} & m = i - 1 & l = n - m holds

b_{5} /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

for R being non empty unital doubleLoopStr

for a, b being Element of R

for n being Nat

for b

( b

b

theorem Th22: :: BINOM:22

for R being non empty unital right_zeroed doubleLoopStr

for a, b being Element of R holds (a,b) In_Power 0 = <*(1_ R)*>

for a, b being Element of R holds (a,b) In_Power 0 = <*(1_ R)*>

proof end;

theorem Th23: :: BINOM:23

for R being non empty unital right_zeroed doubleLoopStr

for a, b being Element of R

for n being Nat holds ((a,b) In_Power n) . 1 = a |^ n

for a, b being Element of R

for n being Nat holds ((a,b) In_Power n) . 1 = a |^ n

proof end;

theorem Th24: :: BINOM:24

for R being non empty unital right_zeroed doubleLoopStr

for a, b being Element of R

for n being Nat holds ((a,b) In_Power n) . (n + 1) = b |^ n

for a, b being Element of R

for n being Nat holds ((a,b) In_Power n) . (n + 1) = b |^ n

proof end;

:: Binomial Theorem

theorem :: BINOM:25

for R being non empty add-cancelable left_zeroed distributive unital associative commutative Abelian add-associative right_zeroed doubleLoopStr

for a, b being Element of R

for n being Element of NAT holds (a + b) |^ n = Sum ((a,b) In_Power n)

for a, b being Element of R

for n being Element of NAT holds (a + b) |^ n = Sum ((a,b) In_Power n)

proof end;

theorem :: BINOM:26

theorem :: BINOM:27