BINOM: The Binomial Theorem for Algebraic Structures

let C, D be non empty set ; :: thesis:
let b be Element of D; :: thesis:
let F be Function of [:C,D:],D; :: thesis:
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:

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)) ) )

proof

let a be Element of C; :: thesis:
defpred S₁[ 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₁[n,x,y] ;
ex f being sequence of D st
( f . 0 = b & ( for n being Nat holds S₁[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:

end;

ex g being Function of C,(Funcs (NAT,D)) st
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

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)) ) ) } ;

A3: now :: thesis:

let x, y1, y2 be object ; :: thesis:
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:
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:

defpred S₁[ Nat] means f1 . $1 = f2 . $1;
let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Element of NAT ;

A18: now :: thesis:

let n be Nat; :: thesis:
assume A19: S₁[n] ; :: thesis:
f1 . (n + 1) = F . (a2,(f1 . n)) by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S₁[n + 1] ; :: thesis:

end;

A20: S₁[ 0 ] by A11, A14;
for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A18);
hence f1 . x = f2 . x9
.= f2 . x ;
:: thesis:

end;

A21: ( NAT = dom f1 & NAT = dom f2 ) by FUNCT_2:def 1;
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:

end;

now :: thesis:

let x be object ; :: thesis:
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:
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:

end;

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)) ) ) } 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

let x be object ; :: thesis:
assume A23: x in C ; :: thesis:
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:

end;

for x being object st x in dom h holds
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)) ) )

proof

let a be Element of C; :: thesis:
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:

end;

hence 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)) ) ) ; :: thesis:

end;

then consider g being Function of C,(Funcs (NAT,D)) such that
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:

let x, y1, y2 be object ; :: thesis:
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:
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:

end;

now :: thesis:

let x be object ; :: thesis:
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:
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:

end;

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 ) } 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

let x be object ; :: thesis:
assume x in [:NAT,C:] ; :: thesis:
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

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

end;

then consider z being Element of D such that
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:

end;

for x being object st x in dom h holds
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))) ) )

proof

let a be Element of C; :: thesis:
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:

let k be Nat; :: thesis:
[(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:

end;

[0,a] in [:NAT,C:] by ZFMISC_1:def 2;
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:

end;

hence 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))) ) ) ; :: thesis:

end;

Lm2: now :: thesis:

let C, D be non empty set ; :: thesis:
let b be Element of D; :: thesis:
let F be Function of [:D,C:],D; :: thesis:
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:

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) ) )

proof

let a be Element of C; :: thesis:
defpred S₁[ 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₁[n,x,y] ;
ex f being sequence of D st
( f . 0 = b & ( for n being Nat holds S₁[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:

end;

ex g being Function of C,(Funcs (NAT,D)) st
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

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) ) ) } ;

A3: now :: thesis:

let x, y1, y2 be object ; :: thesis:
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:
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:

defpred S₁[ Nat] means f1 . $1 = f2 . $1;
let x be object ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider x9 = x as Element of NAT ;

A18: now :: thesis:

let n be Nat; :: thesis:
assume A19: S₁[n] ; :: thesis:
f1 . (n + 1) = F . ((f1 . n),a2) by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S₁[n + 1] ; :: thesis:

end;

A20: S₁[ 0 ] by A11, A14;
for n being Nat holds S₁[n] from NAT_1:sch 2(A20, A18);
hence f1 . x = f2 . x9
.= f2 . x ;
:: thesis:

end;

A21: ( NAT = dom f1 & NAT = dom f2 ) by FUNCT_2:def 1;
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:

end;

now :: thesis:

let x be object ; :: thesis:
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:
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:

end;

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) ) ) } 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

let x be object ; :: thesis:
assume A23: x in C ; :: thesis:
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:

end;

proof

let a be Element of C; :: thesis:
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:

end;

hence 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) ) ) ; :: thesis:

end;

then consider g being Function of C,(Funcs (NAT,D)) such that
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:

let x, y1, y2 be object ; :: thesis:
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:
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:

end;

now :: thesis:

let x be object ; :: thesis:
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:
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:

end;

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 ) } 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

let x be object ; :: thesis:
assume x in [:C,NAT:] ; :: thesis:
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

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

end;

then consider z being Element of D such that
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:

end;

for x being object st x in dom h holds
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) ) )

proof

let a be Element of C; :: thesis:
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:

let k be Element of NAT ; :: thesis:
[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:

end;

[a,0] in [:C,NAT:] by ZFMISC_1:def 2;
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:

end;

hence 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) ) ) ; :: thesis:

end;

theorem Th3: :: BINOM:3

for L being non empty left_zeroed addLoopStr
for a being Element of L holds Sum <*a*> = a

proof end;

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)

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

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

proof end;

definition

let R be non empty addLoopStr ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines + BINOM:def 1 :

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)

proof end;

definition

let R be non empty unital multMagma ;
let a be Element of R;
let n be Nat;

func a |^ n -> Element of R equals :: BINOM:def 2
(power R) . (a,n);

coherence ;

end;

:: deftheorem defines |^ BINOM:def 2 :

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 )

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)

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)

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)

proof end;

definition

let R be non empty addLoopStr ;

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

proof end;

uniqueness

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

proof end;

uniqueness

proof end;

end;

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

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

definition

let R be non empty addLoopStr ;
let a be Element of R;
let n be Nat;

func n * a -> Element of R equals :: BINOM:def 5
(Nat-mult-left R) . (n,a);

coherence ;

func a * n -> Element of R equals :: BINOM:def 6
(Nat-mult-right R) . (a,n);

coherence ;

end;

:: deftheorem defines * BINOM:def 5 :

:: deftheorem defines * BINOM:def 6 :

theorem :: BINOM:12

for R being non empty addLoopStr
for a being Element of R holds
( 0 * a = 0. R & a * 0 = 0. R ) by Def3, Def4;

theorem Th13: :: BINOM:13

for R being non empty right_zeroed addLoopStr
for a being Element of R holds 1 * a = a

proof end;

theorem Th14: :: BINOM:14

for R being non empty left_zeroed addLoopStr
for a being Element of R holds a * 1 = a

proof end;

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)

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)

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

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

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)

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

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)

proof end;

definition

let R be non empty unital doubleLoopStr ;
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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines In_Power BINOM:def 7 :

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)*>

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

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

proof end;

theorem :: BINOM:26

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))) ) ) by Lm1;

theorem :: BINOM:27

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) ) ) by Lm2;