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

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

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

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

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

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

definition
let R be non empty addLoopStr ;
let p, q be FinSequence of the carrier of R;
funcp + q ->  FinSequence of the carrier of R means :Def1: :: BINOM:def 1
( dom it = dom p &amp; ( for i being Nat st 1 <= i &amp; 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 &amp; ( for i being Nat st 1 <= i &amp; i <= len b1 holds
b1 /. i = (p /. i) + (q /. i) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of R st dom b1 = dom p &amp; ( for i being Nat st 1 <= i &amp; i <= len b1 holds
b1 /. i = (p /. i) + (q /. i) ) &amp; dom b2 = dom p &amp; ( for i being Nat st 1 <= i &amp; i <= len b2 holds
b2 /. i = (p /. i) + (q /. i) ) holds
b1 = b2
proofend;
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 &amp; ( for i being Nat st 1 <= i &amp; 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)
proofend;

begin

definition
let R be non empty unital multMagma ;
let a be Element of R;
let n be Nat;
funca |^ n ->  Element of R equals :: BINOM:def 2
(power R) . (a,n);
coherence
 (power R) . (a,n) is Element of R
proofend;
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 &amp; a |^ 1 = a )
proofend;

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

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

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

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

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 &amp; ( 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 &amp; ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) )
proofend;
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 &amp; ( for n being Element of NAT holds b1 . ((n + 1),a) = a + (b1 . (n,a)) ) ) ) &amp; ( for a being Element of R holds
( b2 . (0,a) = 0. R &amp; ( for n being Element of NAT holds b2 . ((n + 1),a) = a + (b2 . (n,a)) ) ) ) holds
b1 = b2
proofend;
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 &amp; ( 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 &amp; ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) )
proofend;
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 &amp; ( for n being Element of NAT holds b1 . (a,(n + 1)) = (b1 . (a,n)) + a ) ) ) &amp; ( for a being Element of R holds
( b2 . (a,0) = 0. R &amp; ( for n being Element of NAT holds b2 . (a,(n + 1)) = (b2 . (a,n)) + a ) ) ) holds
b1 = b2
proofend;
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 &amp; ( 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 &amp; ( 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 ;
funcn * 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 ;
funca * 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 &amp; 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
proofend;

theorem Th14: :: BINOM:14
for R being non empty left_zeroed addLoopStr
for a being Element of R holds a * 1 = a
proofend;

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

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

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

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

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

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

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

begin

definition
let k, n be Element of NAT ;
:: original:choose
redefine funcn 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 &amp; ( for i, l, m being Element of NAT st i in dom it &amp; m = i - 1 &amp; 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 &amp; ( for i, l, m being Element of NAT st i in dom b1 &amp; m = i - 1 &amp; l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of the carrier of R st len b1 = n + 1 &amp; ( for i, l, m being Element of NAT st i in dom b1 &amp; m = i - 1 &amp; l = n - m holds
b1 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) &amp; len b2 = n + 1 &amp; ( for i, l, m being Element of NAT st i in dom b2 &amp; m = i - 1 &amp; l = n - m holds
b2 /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) holds
b1 = b2
proofend;
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 &amp; ( for i, l, m being Element of NAT st i in dom b5 &amp; m = i - 1 &amp; 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)*>
proofend;

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

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

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

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