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


begin

registration
cluster non empty right_add-cancelable Abelian -> non empty left_add-cancelable for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is Abelian & b1 is right_add-cancelable holds
b1 is left_add-cancelable
proof end;
cluster non empty left_add-cancelable Abelian -> non empty right_add-cancelable for addLoopStr ;
coherence
for b1 being non empty addLoopStr st b1 is Abelian & b1 is left_add-cancelable holds
b1 is right_add-cancelable
proof end;
end;

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

registration
cluster non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed for doubleLoopStr ;
existence
ex b1 being non empty doubleLoopStr st
( b1 is Abelian & b1 is add-associative & b1 is left_zeroed & b1 is right_zeroed & b1 is commutative & b1 is associative & b1 is add-cancelable & b1 is distributive & b1 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 :: 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 Element of 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 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 S1[ 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 S1[n,x,y] ;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds S1[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 :: thesis: for x, y1, y2 being set st [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)) ) ) } holds
y1 = y2
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 = [a1,l1] `1
.= [x,y1] `1 by A6
.= x
.= [x,y2] `1
.= [a2,l2] `1 by A8
.= a2 ;
A17: now :: thesis: for x being set st x in NAT holds
f1 . x = f2 . x
defpred S1[ 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 :: thesis: for n being Element of NAT st S1[n] holds
S1[n + 1]
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A19: S1[n] ; :: thesis: S1[n + 1]
f1 . (n + 1) = F . (a2,(f1 . n)) by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S1[n + 1] ; :: thesis: verum
end;
A20: S1[ 0 ] by A11, A14;
for n being Element of NAT holds S1[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 = [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;
now :: thesis: for x being set st 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)) ) ) } holds
x in [:C,(Funcs (NAT,D)):]
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:8;
[x,f9] in h by A23, A24;
hence x in dom h by XTUPLE_0:def 12; :: thesis: verum
end;
for x being set st x in dom h holds
x in C ;
then dom h = C by A22, TARSKI:1;
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: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 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 = [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 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 :: thesis: for x, y1, y2 being set 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 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 ) } holds
y1 = y2
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] = [[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;
now :: thesis: for x being set 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 Function of NAT,D st
( f = g . a & z = f . n ) } holds
x in [:[:NAT,C:],D:]
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
A39: 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 A39, 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;
A40: 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
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 Function of NAT,D such that
A44: 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 A44; :: thesis: verum
end;
then consider z being Element of D such that
A45: ex f being Function of NAT,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;
for x being set st x in dom h holds
x in [:NAT,C:] ;
then dom h = [:NAT,C:] by A40, TARSKI:1;
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
A46: g . a = f9 and
A47: f9 . 0 = b and
A48: for n being Element of NAT holds f9 . (n + 1) = F . (a,(f9 . n)) by A28;
A49: now :: thesis: for k being Element of NAT holds h . ((k + 1),a) = F . (a,(h . (k,a)))
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
A50: [[(k + 1),a],u] in h by XTUPLE_0:def 12;
[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
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 Function of NAT,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 Function of NAT,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;
[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
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 Function of NAT,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 Element of 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;
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 :: 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) ) )
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 S1[ 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 S1[n,x,y] ;
ex f being Function of NAT,D st
( f . 0 = b & ( for n being Element of NAT holds S1[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 :: thesis: for x, y1, y2 being set st [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) ) ) } holds
y1 = y2
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 = [a1,l1] `1
.= [x,y1] `1 by A6
.= x
.= [x,y2] `1
.= [a2,l2] `1 by A8
.= a2 ;
A17: now :: thesis: for x being set st x in NAT holds
f1 . x = f2 . x
defpred S1[ 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 :: thesis: for n being Element of NAT st S1[n] holds
S1[n + 1]
let n be Element of NAT ; :: thesis: ( S1[n] implies S1[n + 1] )
assume A19: S1[n] ; :: thesis: S1[n + 1]
f1 . (n + 1) = F . ((f1 . n),a2) by A12, A16
.= f2 . (n + 1) by A15, A19 ;
hence S1[n + 1] ; :: thesis: verum
end;
A20: S1[ 0 ] by A11, A14;
for n being Element of NAT holds S1[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 = [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;
now :: thesis: for x being set st 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) ) ) } holds
x in [:C,(Funcs (NAT,D)):]
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:8;
[x,f9] in h by A23, A24;
hence x in dom h by XTUPLE_0:def 12; :: thesis: verum
end;
for x being set st x in dom h holds
x in C ;
then dom h = C by A22, TARSKI:1;
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: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 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 = [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 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 :: thesis: for x, y1, y2 being set 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 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 ) } holds
y1 = y2
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] = [[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;
now :: thesis: for x being set 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 Function of NAT,D st
( f = g . a & z = f . n ) } holds
x in [:[:C,NAT:],D:]
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
A39: 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 A39, 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;
A40: 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
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 Function of NAT,D such that
A44: 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 A44; :: thesis: verum
end;
then consider z being Element of D such that
A45: ex f being Function of NAT,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;
for x being set st x in dom h holds
x in [:C,NAT:] ;
then dom h = [:C,NAT:] by A40, TARSKI:1;
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
A46: g . a = f9 and
A47: f9 . 0 = b and
A48: for n being Element of 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)
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
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 set 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 Function of NAT,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 Function of NAT,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 Function of NAT,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,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
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 Function of NAT,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;
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
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
ex b1 being FinSequence of the carrier of R st
( dom b1 = dom p & ( for i being Nat st 1 <= i & i <= len b1 holds
b1 /. i = (p /. i) + (q /. i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st dom b1 = dom p & ( for i being Nat st 1 <= i & i <= len b1 holds
b1 /. i = (p /. i) + (q /. i) ) & dom b2 = dom p & ( for i being Nat st 1 <= i & i <= len b2 holds
b2 /. i = (p /. i) + (q /. i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines + BINOM:def 1 :
for R being non empty addLoopStr
for p, q, b4 being FinSequence of the carrier of R holds
( b4 = p + q iff ( dom b4 = dom p & ( for i being Nat st 1 <= i & i <= len b4 holds
b4 /. 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 2
(power R) . (a,n);
coherence
(power R) . (a,n) is Element of R
proof end;
end;

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

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;

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

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 :Def3: :: BINOM:def 3
 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 b1 being Function of [:NAT, the carrier of R:], the carrier of R st
for a being Element of R holds
( b1 . (0,a) = 0. R & ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) )
proof end;
uniqueness
for b1, b2 being Function of [:NAT, the carrier of R:], the carrier of R st ( for a being Element of R holds
( b1 . (0,a) = 0. R & ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) ) ) & ( for a being Element of R holds
( b2 . (0,a) = 0. R & ( for n being Element of NAT holds b2 . ((n + 1),a) = a + (b2 . (n,a)) ) ) ) holds
b1 = b2
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
ex b1 being Function of [: the carrier of R,NAT:], the carrier of R st
for a being Element of R holds
( b1 . (a,0) = 0. R & ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) )
proof end;
uniqueness
for b1, b2 being Function of [: the carrier of R,NAT:], the carrier of R st ( for a being Element of R holds
( b1 . (a,0) = 0. R & ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) ) ) & ( for a being Element of R holds
( b2 . (a,0) = 0. R & ( for n being Element of NAT holds b2 . (a,(n + 1)) = (b2 . (a,n)) + a ) ) ) holds
b1 = b2
proof end;
end;

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

:: deftheorem Def4 defines Nat-mult-right BINOM:def 4 :
for R being non empty addLoopStr
for b2 being Function of [: the carrier of R,NAT:], the carrier of R holds
( b2 = Nat-mult-right R iff for a being Element of R holds
( b2 . (a,0) = 0. R & ( for n being Element of NAT holds b2 . (a,(n + 1)) = (b2 . (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 5
(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 6
(Nat-mult-right R) . (a,n);
coherence
(Nat-mult-right R) . (a,n) is Element of R ;
end;

:: deftheorem defines * BINOM:def 5 :
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 6 :
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: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 Element of 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;

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:25;
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 :Def7: :: BINOM:def 7
( 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 b1 being FinSequence of the carrier of R st
( len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of R st len b1 = n + 1 & ( for i, l, m being Element of NAT st i in dom b1 & m = i - 1 & l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len b2 = n + 1 & ( for i, l, m being Element of NAT st i in dom b2 & m = i - 1 & l = n - m holds
b2 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
proof end;
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 Element of NAT
for b5 being FinSequence of the carrier of R holds
( b5 = (a,b) In_Power n iff ( len b5 = n + 1 & ( for i, l, m being Element of NAT st i in dom b5 & m = i - 1 & l = n - m holds
b5 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) );

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 Element of 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 Element of NAT holds ((a,b) In_Power n) . (n + 1) = b |^ n
proof end;

:: WP: Binomial Theorem
theorem :: BINOM:25
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: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 Element of 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;