:: The Binomial Theorem for Algebraic Structures
:: by Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

registration

cluster non empty right_add-cancelable Abelian -> non empty left_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Abelian & b₁ is right_add-cancelable holds
b₁ is left_add-cancelable

proof end;

cluster non empty left_add-cancelable Abelian -> non empty right_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is Abelian & b₁ is left_add-cancelable holds
b₁ is right_add-cancelable

proof end;

end;

registration

cluster non empty right_complementable add-associative right_zeroed -> non empty right_add-cancelable addLoopStr ;
coherence
for b₁ being non empty addLoopStr st b₁ is right_zeroed & b₁ is right_complementable & b₁ is add-associative holds
b₁ is right_add-cancelable ;

end;

registration

cluster non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed doubleLoopStr ;
existence
ex b₁ being non empty doubleLoopStr st
( b₁ is Abelian & b₁ is add-associative & b₁ is left_zeroed & b₁ is right_zeroed & b₁ is commutative & b₁ is associative & b₁ is add-cancelable & b₁ is distributive & b₁ is unital )

proof end;

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

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

proof end;

Lm1: now

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 Element of 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 Element of 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 Element of 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 Element of NAT holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) ) :: thesis: verum

proof

A1: for a being Element of C ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )

proof

let a be Element of C; :: thesis: ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )
defpred S₁[ Element of NAT , Element of D, Element of D] means $3 = F . (a,$2);
A2: for n being Element of NAT
for x being Element of D ex y being Element of D st S₁[n,x,y] ;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
hence ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

end;

ex g being Function of C,(Funcs (NAT,D)) st
for a being Element of C ex f being Function of NAT,D st
( g . a = f & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } ;

A3: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l1 & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l2 & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a2,(f . n)) ) ) by A5;
consider f1 being Function of NAT,D such that
A10: f1 = l1 and
A11: f1 . 0 = b and
A12: for n being Element of NAT holds f1 . (n + 1) = F . (a1,(f1 . n)) by A7;
consider f2 being Function of NAT,D such that
A13: f2 = l2 and
A14: f2 . 0 = b and
A15: for n being Element of NAT holds f2 . (n + 1) = F . (a2,(f2 . n)) by A9;
A16: a1 = [x,y1] `1 by A6, MCART_1:def 1
.= x by MCART_1:def 1
.= [a2,l2] `1 by A8, MCART_1:def 1
.= a2 by MCART_1:def 1 ;

A17: now

defpred S₁[ Element of NAT ] means f1 . $1 = f2 . $1;
let x be set ; :: 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

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

end;

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

end;

A21: ( NAT = dom f1 & NAT = dom f2 ) by FUNCT_2:def 1;
thus y1 = [a1,l1] `2 by A6, MCART_1:def 2
.= l1 by MCART_1:def 2
.= l2 by A10, A13, A21, A17, FUNCT_1:9
.= [x,y2] `2 by A8, MCART_1:def 2
.= y2 by MCART_1:def 2 ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) ) ;
hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;
A22: for x being set st x in C holds
x in dom h

proof

let x be set ; :: thesis: ( x in C implies x in dom h )
assume A23: x in C ; :: thesis: x in dom h
then consider f being Function of NAT,D such that
A24: ( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (x,(f . n)) ) ) by A1;
reconsider f9 = f as Element of Funcs (NAT,D) by FUNCT_2:11;
[x,f9] in h by A23, A24;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set 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 Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )
for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) )

proof

let a be Element of C; :: thesis: ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of 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:8;
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 Function of NAT,D st
( f9 = l & f9 . 0 = b & ( for n being Element of NAT holds f9 . (n + 1) = F . (a9,(f9 . n)) ) ) ;
A27: h . a = [a9,l] `2 by A25, MCART_1:def 2
.= l by MCART_1:def 2 ;
a = [a9,l] `1 by A25, MCART_1:def 1
.= a9 by MCART_1:def 1 ;
hence ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) by A26, A27; :: thesis: verum

end;

hence for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . (a,(f . n)) ) ) ; :: thesis: verum

end;

then consider g being Function of C,(Funcs (NAT,D)) such that
A28: for a being Element of C ex f being Function of NAT,D st
( g . a = f & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = g . a & z = f . n ) } ;

A29: now

let x, y1, y2 be set ; :: 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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,D st
( f2 = g . a2 & z2 = f2 . n2 ) by A31;
A36: [n1,a1] = [x,y1] `1 by A32, MCART_1:def 1
.= x by MCART_1:def 1
.= [[n2,a2],z2] `1 by A34, MCART_1:def 1
.= [n2,a2] by MCART_1:def 1 ;
then A37: a1 = [n2,a2] `2 by MCART_1:def 2
.= a2 by MCART_1:def 2 ;
n1 = [n2,a2] `1 by A36, MCART_1:def 1
.= n2 by MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A32, A33, A34, A35, A37, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

now

let x be set ; :: 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 Function of NAT,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 Function of NAT,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
A38: x = [[n1,a1],z1] and
ex f1 being Function of NAT,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 A38, ZFMISC_1:def 2; :: thesis: verum

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 Function of NAT,D st
( f = g . a & z = f . n ) } as Relation of [:NAT,C:],D by TARSKI:def 3;
A39: for x being set st x in [:NAT,C:] holds
x in dom h

proof

let x be set ; :: 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 set such that
A40: n in NAT and
A41: d in C and
A42: x = [n,d] by ZFMISC_1:def 2;
reconsider d = d as Element of C by A41;
reconsider n = n as Element of NAT by A40;
consider f9 being Function of NAT,D such that
A43: g . d = f9 and
f9 . 0 = b and
for n being Element of NAT holds f9 . (n + 1) = F . (d,(f9 . n)) by A28;
ex z being Element of D ex f being Function of NAT,D st
( f = g . d & z = f . n )

proof

take f9 . n ; :: thesis: ex f being Function of NAT,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 A43; :: thesis: verum

end;

then consider z being Element of D such that
A44: ex f being Function of NAT,D st
( f = g . d & z = f . n ) ;
[x,z] in h by A42, A44;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set st x in dom h holds
x in [:NAT,C:] ;
then dom h = [:NAT,C:] by A39, 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 Element of 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 Element of NAT holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )

proof

let a be Element of C; :: thesis: ( h . (0,a) = b & ( for n being Element of NAT holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) )
consider f9 being Function of NAT,D such that
A45: g . a = f9 and
A46: f9 . 0 = b and
A47: for n being Element of NAT holds f9 . (n + 1) = F . (a,(f9 . n)) by A28;

A48: now

let k be Element of 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 set such that
A49: [[(k + 1),a],u] in h by RELAT_1:def 4;
[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 set such that
A50: [[k,a],v] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of C, z being Element of D such that
A51: [[(k + 1),a],u] = [[n,d],z] and
A52: ex f1 being Function of NAT,D st
( f1 = g . d & z = f1 . n ) by A49;
A53: u = [[n,d],z] `2 by A51, MCART_1:def 2
.= z by MCART_1:def 2 ;
consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that
A54: [[k,a],v] = [[n1,d1],z1] and
A55: ex f2 being Function of NAT,D st
( f2 = g . d1 & z1 = f2 . n1 ) by A50;
A56: v = [[n1,d1],z1] `2 by A54, MCART_1:def 2
.= z1 by MCART_1:def 2 ;
A57: [(k + 1),a] = [[n,d],z] `1 by A51, MCART_1:def 1
.= [n,d] by MCART_1:def 1 ;
then A58: d = [(k + 1),a] `2 by MCART_1:def 2
.= a by MCART_1:def 2 ;
A59: [k,a] = [[n1,d1],z1] `1 by A54, MCART_1:def 1
.= [n1,d1] by MCART_1:def 1 ;
then A60: n1 = [k,a] `1 by MCART_1:def 1
.= k by MCART_1:def 1 ;
A61: d1 = [k,a] `2 by A59, MCART_1:def 2
.= a by MCART_1:def 2 ;
n = [(k + 1),a] `1 by A57, MCART_1:def 1
.= k + 1 by MCART_1:def 1 ;
hence h . ((k + 1),a) = f9 . (k + 1) by A45, A49, A52, A53, A58, FUNCT_1:8
.= F . (a,z1) by A45, A47, A55, A60, A61
.= F . (a,(h . (k,a))) by A50, A56, FUNCT_1:8 ;
:: thesis: verum

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 set such that
A62: [[0,a],u] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of C, z being Element of D such that
A63: [[0,a],u] = [[n,d],z] and
A64: ex f1 being Function of NAT,D st
( f1 = g . d & z = f1 . n ) by A62;
A65: u = [[n,d],z] `2 by A63, MCART_1:def 2
.= z by MCART_1:def 2 ;
A66: [0,a] = [[n,d],z] `1 by A63, MCART_1:def 1
.= [n,d] by MCART_1:def 1 ;
then A67: d = [0,a] `2 by MCART_1:def 2
.= a by MCART_1:def 2 ;
n = [0,a] `1 by A66, MCART_1:def 1
.= 0 by MCART_1:def 1 ;
hence ( h . (0,a) = b & ( for n being Element of NAT holds h . ((n + 1),a) = F . (a,(h . (n,a))) ) ) by A45, A46, A62, A64, A65, A67, A48, FUNCT_1:8; :: thesis: verum

end;

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

end;

end;

Lm2: now

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

proof

A1: for a being Element of C ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )

proof

let a be Element of C; :: thesis: ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )
defpred S₁[ Element of NAT , Element of D, Element of D] means $3 = F . ($2,a);
A2: for n being Element of NAT
for x being Element of D ex y being Element of D st S₁[n,x,y] ;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 2(A2);
hence ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

end;

ex g being Function of C,(Funcs (NAT,D)) st
for a being Element of C ex f being Function of NAT,D st
( g . a = f & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } ;

A3: now

let x, y1, y2 be set ; :: thesis: ( [x,y1] in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l1 & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l2 & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a2) ) ) by A5;
consider f1 being Function of NAT,D such that
A10: f1 = l1 and
A11: f1 . 0 = b and
A12: for n being Element of NAT holds f1 . (n + 1) = F . ((f1 . n),a1) by A7;
consider f2 being Function of NAT,D such that
A13: f2 = l2 and
A14: f2 . 0 = b and
A15: for n being Element of NAT holds f2 . (n + 1) = F . ((f2 . n),a2) by A9;
A16: a1 = [x,y1] `1 by A6, MCART_1:def 1
.= x by MCART_1:def 1
.= [a2,l2] `1 by A8, MCART_1:def 1
.= a2 by MCART_1:def 1 ;

A17: now

defpred S₁[ Element of NAT ] means f1 . $1 = f2 . $1;
let x be set ; :: 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

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

end;

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

end;

A21: ( NAT = dom f1 & NAT = dom f2 ) by FUNCT_2:def 1;
thus y1 = [a1,l1] `2 by A6, MCART_1:def 2
.= l1 by MCART_1:def 2
.= l2 by A10, A13, A21, A17, FUNCT_1:9
.= [x,y2] `2 by A8, MCART_1:def 2
.= y2 by MCART_1:def 2 ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( x in { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) ) ;
hence x in [:C,(Funcs (NAT,D)):] by ZFMISC_1:def 2; :: thesis: verum

end;

then reconsider h = { [a,l] where a is Element of C, l is Element of Funcs (NAT,D) : ex f being Function of NAT,D st
( f = l & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) } as Relation of C,(Funcs (NAT,D)) by TARSKI:def 3;
A22: for x being set st x in C holds
x in dom h

proof

let x be set ; :: thesis: ( x in C implies x in dom h )
assume A23: x in C ; :: thesis: x in dom h
then consider f being Function of NAT,D such that
A24: ( f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),x) ) ) by A1;
reconsider f9 = f as Element of Funcs (NAT,D) by FUNCT_2:11;
[x,f9] in h by A23, A24;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set 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 Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )
for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) )

proof

let a be Element of C; :: thesis: ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of 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:8;
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 Function of NAT,D st
( f9 = l & f9 . 0 = b & ( for n being Element of NAT holds f9 . (n + 1) = F . ((f9 . n),a9) ) ) ;
A27: h . a = [a9,l] `2 by A25, MCART_1:def 2
.= l by MCART_1:def 2 ;
a = [a9,l] `1 by A25, MCART_1:def 1
.= a9 by MCART_1:def 1 ;
hence ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) by A26, A27; :: thesis: verum

end;

hence for a being Element of C ex f being Function of NAT,D st
( h . a = f & f . 0 = b & ( for n being Element of NAT holds f . (n + 1) = F . ((f . n),a) ) ) ; :: thesis: verum

end;

then consider g being Function of C,(Funcs (NAT,D)) such that
A28: for a being Element of C ex f being Function of NAT,D st
( g . a = f & f . 0 = b & ( for n being Element of 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 Function of NAT,D st
( f = g . a & z = f . n ) } ;

A29: now

let x, y1, y2 be set ; :: 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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,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 Function of NAT,D st
( f2 = g . a2 & z2 = f2 . n2 ) by A31;
A36: [a1,n1] = [x,y1] `1 by A32, MCART_1:def 1
.= x by MCART_1:def 1
.= [[a2,n2],z2] `1 by A34, MCART_1:def 1
.= [a2,n2] by MCART_1:def 1 ;
then A37: n1 = [a2,n2] `2 by MCART_1:def 2
.= n2 by MCART_1:def 2 ;
a1 = [a2,n2] `1 by A36, MCART_1:def 1
.= a2 by MCART_1:def 1 ;
hence y1 = [x,y2] `2 by A32, A33, A34, A35, A37, MCART_1:def 2
.= y2 by MCART_1:def 2 ;
:: thesis: verum

end;

now

let x be set ; :: 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 Function of NAT,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 Function of NAT,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
A38: x = [[a1,n1],z1] and
ex f1 being Function of NAT,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 A38, ZFMISC_1:def 2; :: thesis: verum

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 Function of NAT,D st
( f = g . a & z = f . n ) } as Relation of [:C,NAT:],D by TARSKI:def 3;
A39: for x being set st x in [:C,NAT:] holds
x in dom h

proof

let x be set ; :: 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 set such that
A40: d in C and
A41: n in NAT and
A42: x = [d,n] by ZFMISC_1:def 2;
reconsider d = d as Element of C by A40;
reconsider n = n as Element of NAT by A41;
consider f9 being Function of NAT,D such that
A43: g . d = f9 and
f9 . 0 = b and
for n being Element of NAT holds f9 . (n + 1) = F . ((f9 . n),d) by A28;
ex z being Element of D ex f being Function of NAT,D st
( f = g . d & z = f . n )

proof

take f9 . n ; :: thesis: ex f being Function of NAT,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 A43; :: thesis: verum

end;

then consider z being Element of D such that
A44: ex f being Function of NAT,D st
( f = g . d & z = f . n ) ;
[x,z] in h by A42, A44;
hence x in dom h by RELAT_1:def 4; :: thesis: verum

end;

for x being set st x in dom h holds
x in [:C,NAT:] ;
then dom h = [:C,NAT:] by A39, 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

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 Function of NAT,D such that
A45: g . a = f9 and
A46: f9 . 0 = b and
A47: for n being Element of NAT holds f9 . (n + 1) = F . ((f9 . n),a) by A28;

A48: now

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 set such that
A49: [[a,(k + 1)],u] in h by RELAT_1:def 4;
[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 set such that
A50: [[a,k],v] in h by RELAT_1:def 4;
consider n1 being Element of NAT , d1 being Element of C, z1 being Element of D such that
A51: [[a,k],v] = [[d1,n1],z1] and
A52: ex f2 being Function of NAT,D st
( f2 = g . d1 & z1 = f2 . n1 ) by A50;
A53: v = [[d1,n1],z1] `2 by A51, MCART_1:def 2
.= z1 by MCART_1:def 2 ;
A54: [a,k] = [[d1,n1],z1] `1 by A51, MCART_1:def 1
.= [d1,n1] by MCART_1:def 1 ;
then A55: n1 = [a,k] `2 by MCART_1:def 2
.= k by MCART_1:def 2 ;
consider f2 being Function of NAT,D such that
A56: f2 = g . d1 and
A57: z1 = f2 . n1 by A52;
consider n being Element of NAT , d being Element of C, z being Element of D such that
A58: [[a,(k + 1)],u] = [[d,n],z] and
A59: ex f1 being Function of NAT,D st
( f1 = g . d & z = f1 . n ) by A49;
A60: [a,(k + 1)] = [[d,n],z] `1 by A58, MCART_1:def 1
.= [d,n] by MCART_1:def 1 ;
then A61: n = [a,(k + 1)] `2 by MCART_1:def 2
.= k + 1 by MCART_1:def 2 ;
A62: d1 = [a,k] `1 by A54, MCART_1:def 1
.= a by MCART_1:def 1 ;
A63: d = [a,(k + 1)] `1 by A60, MCART_1:def 1
.= a by MCART_1:def 1 ;
u = [[d,n],z] `2 by A58, MCART_1:def 2
.= z by MCART_1:def 2 ;
hence h . (a,(k + 1)) = f9 . n by A45, A49, A59, A63, FUNCT_1:8
.= F . ((f2 . n1),a) by A45, A47, A61, A56, A55, A62
.= F . ((h . (a,k)),a) by A50, A57, A53, FUNCT_1:8 ;
:: thesis: verum

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 set such that
A64: [[a,0],u] in h by RELAT_1:def 4;
consider n being Element of NAT , d being Element of C, z being Element of D such that
A65: [[a,0],u] = [[d,n],z] and
A66: ex f1 being Function of NAT,D st
( f1 = g . d & z = f1 . n ) by A64;
A67: u = [[d,n],z] `2 by A65, MCART_1:def 2
.= z by MCART_1:def 2 ;
A68: [a,0] = [[d,n],z] `1 by A65, MCART_1:def 1
.= [d,n] by MCART_1:def 1 ;
then A69: d = [a,0] `1 by MCART_1:def 1
.= a by MCART_1:def 1 ;
n = [a,0] `2 by A68, MCART_1:def 2
.= 0 by MCART_1:def 2 ;
hence ( h . (a,0) = b & ( for n being Element of NAT holds h . (a,(n + 1)) = F . ((h . (a,n)),a) ) ) by A45, A46, A64, A66, A67, A69, A48, FUNCT_1:8; :: thesis: verum

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: verum

end;

end;

begin

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

canceled;
canceled;
canceled;
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 :Def4: :: BINOM:def 4
( dom it = dom p & ( for i being Nat st 1 <= i & i <= len it holds
it /. i = (p /. i) + (q /. i) ) );
existence
ex b₁ being FinSequence of the carrier of R st
( dom b₁ = dom p & ( for i being Nat st 1 <= i & i <= len b₁ holds
b₁ /. i = (p /. i) + (q /. i) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of R st dom b₁ = dom p & ( for i being Nat st 1 <= i & i <= len b₁ holds
b₁ /. i = (p /. i) + (q /. i) ) & dom b₂ = dom p & ( for i being Nat st 1 <= i & i <= len b₂ holds
b₂ /. i = (p /. i) + (q /. i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem BINOM:def 1 :
canceled;

:: deftheorem BINOM:def 2 :
canceled;

:: deftheorem BINOM:def 3 :
canceled;

:: deftheorem Def4 defines + BINOM:def 4 :
for R being non empty addLoopStr
for p, q, b₄ being FinSequence of the carrier of R holds
( b₄ = p + q iff ( dom b₄ = dom p & ( for i being Nat st 1 <= i & i <= len b₄ holds
b₄ /. i = (p /. i) + (q /. i) ) ) );

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;

begin

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 5
(power R) . (a,n);
coherence
(power R) . (a,n) is Element of R

proof end;

end;

:: deftheorem defines |^ BINOM:def 5 :
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 )

proof end;

theorem :: BINOM:9

canceled;

theorem :: BINOM:10

for R being non empty unital associative commutative multMagma
for a, b being Element of R
for n being Element of NAT holds (a * b) |^ n = (a |^ n) * (b |^ n)

proof end;

theorem Th11: :: BINOM:11

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 :: BINOM:12

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

proof end;

begin

definition

let R be non empty addLoopStr ;
func Nat-mult-left R -> Function of [:NAT, the carrier of R:], the carrier of R means :Def6: :: BINOM:def 6
for a being Element of R holds
( it . (0,a) = 0. R & ( for n being Element of NAT holds it . ((n + 1),a) = a + (it . (n,a)) ) );
existence
ex b₁ being Function of [:NAT, the carrier of R:], the carrier of R st
for a being Element of R holds
( b₁ . (0,a) = 0. R & ( for n being Element of NAT holds b₁ . ((n + 1),a) = a + (b₁ . (n,a)) ) )

proof end;

uniqueness
for b₁, b₂ being Function of [:NAT, the carrier of R:], the carrier of R st ( for a being Element of R holds
( b₁ . (0,a) = 0. R & ( for n being Element of NAT holds b₁ . ((n + 1),a) = a + (b₁ . (n,a)) ) ) ) & ( for a being Element of R holds
( b₂ . (0,a) = 0. R & ( for n being Element of NAT holds b₂ . ((n + 1),a) = a + (b₂ . (n,a)) ) ) ) holds
b₁ = b₂

proof end;

func Nat-mult-right R -> Function of [: the carrier of R,NAT:], the carrier of R means :Def7: :: BINOM:def 7
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
ex b₁ being Function of [: the carrier of R,NAT:], the carrier of R st
for a being Element of R holds
( b₁ . (a,0) = 0. R & ( for n being Element of NAT holds b₁ . (a,(n + 1)) = (b₁ . (a,n)) + a ) )

proof end;

uniqueness
for b₁, b₂ being Function of [: the carrier of R,NAT:], the carrier of R st ( for a being Element of R holds
( b₁ . (a,0) = 0. R & ( for n being Element of NAT holds b₁ . (a,(n + 1)) = (b₁ . (a,n)) + a ) ) ) & ( for a being Element of R holds
( b₂ . (a,0) = 0. R & ( for n being Element of NAT holds b₂ . (a,(n + 1)) = (b₂ . (a,n)) + a ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Nat-mult-left BINOM:def 6 :
for R being non empty addLoopStr
for b₂ being Function of [:NAT, the carrier of R:], the carrier of R holds
( b₂ = Nat-mult-left R iff for a being Element of R holds
( b₂ . (0,a) = 0. R & ( for n being Element of NAT holds b₂ . ((n + 1),a) = a + (b₂ . (n,a)) ) ) );

:: deftheorem Def7 defines Nat-mult-right BINOM:def 7 :
for R being non empty addLoopStr
for b₂ being Function of [: the carrier of R,NAT:], the carrier of R holds
( b₂ = Nat-mult-right R iff for a being Element of R holds
( b₂ . (a,0) = 0. R & ( for n being Element of NAT holds b₂ . (a,(n + 1)) = (b₂ . (a,n)) + a ) ) );

definition

let R be non empty addLoopStr ;
let a be Element of R;
let n be Element of NAT ;
func n * a -> Element of R equals :: BINOM:def 8
(Nat-mult-left R) . (n,a);
coherence
(Nat-mult-left R) . (n,a) is Element of R ;
func a * n -> Element of R equals :: BINOM:def 9
(Nat-mult-right R) . (a,n);
coherence
(Nat-mult-right R) . (a,n) is Element of R ;

end;

:: deftheorem defines * BINOM:def 8 :
for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds n * a = (Nat-mult-left R) . (n,a);

:: deftheorem defines * BINOM:def 9 :
for R being non empty addLoopStr
for a being Element of R
for n being Element of NAT holds a * n = (Nat-mult-right R) . (a,n);

theorem :: BINOM:13

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

theorem Th14: :: BINOM:14

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

proof end;

theorem Th15: :: BINOM:15

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

proof end;

theorem Th16: :: BINOM:16

for R being non empty left_zeroed add-associative addLoopStr
for a being Element of R
for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)

proof end;

theorem Th17: :: BINOM:17

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 Th18: :: BINOM:18

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:19

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 Th20: :: BINOM:20

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 Th21: :: BINOM:21

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 Th22: :: BINOM:22

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;

begin

definition

let k, n be Element of NAT ;
:: original: choose
redefine func n choose k -> Element of NAT ;
coherence
n choose k is Element of NAT by NEWTON:35;

end;

definition

let R be non empty unital doubleLoopStr ;
let a, b be Element of R;
let n be Element of NAT ;
func (a,b) In_Power n -> FinSequence of the carrier of R means :Def10: :: BINOM:def 10
( len it = n + 1 & ( for i, l, m being Element of NAT st i in dom it & m = i - 1 & l = n - m holds
it /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) );
existence
ex b₁ being FinSequence of the carrier of R st
( len b₁ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of R st len b₁ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₁ & m = i - 1 & l = n - m holds
b₁ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b₂ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₂ & m = i - 1 & l = n - m holds
b₂ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines In_Power BINOM:def 10 :
for R being non empty unital doubleLoopStr
for a, b being Element of R
for n being Element of NAT
for b₅ being FinSequence of the carrier of R holds
( b₅ = (a,b) In_Power n iff ( len b₅ = n + 1 & ( for i, l, m being Element of NAT st i in dom b₅ & m = i - 1 & l = n - m holds
b₅ /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

theorem Th23: :: BINOM:23

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 Th24: :: BINOM:24

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds ((a,b) In_Power n) . 1 = a |^ n

proof end;

theorem Th25: :: BINOM:25

for R being non empty unital right_zeroed doubleLoopStr
for a, b being Element of R
for n being Element of NAT holds ((a,b) In_Power n) . (n + 1) = b |^ n

proof end;

theorem :: BINOM:26

for R being non empty add-cancelable left_zeroed unital associative commutative distributive 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)

proof end;

theorem :: BINOM:27

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 Element of NAT holds g . ((n + 1),a) = F . (a,(g . (n,a))) ) ) by Lm1;

theorem :: BINOM:28

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;