:: BINOM semantic presentation
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
let R be non empty addLoopStr ; ::_thesis: ( R is Abelian & R is right_add-cancelable implies R is left_add-cancelable )
assume ( R is Abelian & R is right_add-cancelable ) ; ::_thesis: R is left_add-cancelable
then reconsider R = R as non empty right_add-cancelable Abelian addLoopStr ;
R is left_add-cancelable
proof
let a, b, c be Element of R; :: according to ALGSTR_0:def_3,ALGSTR_0:def_6 ::_thesis: ( not a + b = a + c or b = c )
assume a + b = a + c ; ::_thesis: b = c
hence b = c by ALGSTR_0:def_4; ::_thesis: verum
end;
hence R is left_add-cancelable ; ::_thesis: verum
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
let R be non empty addLoopStr ; ::_thesis: ( R is Abelian & R is left_add-cancelable implies R is right_add-cancelable )
assume ( R is Abelian & R is left_add-cancelable ) ; ::_thesis: R is right_add-cancelable
then reconsider R = R as non empty left_add-cancelable Abelian addLoopStr ;
R is right_add-cancelable
proof
let a, b, c be Element of R; :: according to ALGSTR_0:def_4,ALGSTR_0:def_7 ::_thesis: ( not b + a = c + a or b = c )
assume b + a = c + a ; ::_thesis: b = c
hence b = c by ALGSTR_0:def_3; ::_thesis: verum
end;
hence R is right_add-cancelable ; ::_thesis: verum
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
set R = the comRing;
take the comRing ; ::_thesis: ( the comRing is Abelian & the comRing is add-associative & the comRing is left_zeroed & the comRing is right_zeroed & the comRing is commutative & the comRing is associative & the comRing is add-cancelable & the comRing is distributive & the comRing is unital )
thus ( the comRing is Abelian & the comRing is add-associative & the comRing is left_zeroed & the comRing is right_zeroed & the comRing is commutative & the comRing is associative & the comRing is add-cancelable & the comRing is distributive & the comRing is unital ) ; ::_thesis: verum
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
let R be non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr ; ::_thesis: for a being Element of R holds (0. R) * a = 0. R
let a be Element of R; ::_thesis: (0. R) * a = 0. R
(0. R) * a = ((0. R) + (0. R)) * a by RLVECT_1:def_4
.= ((0. R) * a) + ((0. R) * a) by VECTSP_1:def_3 ;
then ((0. R) * a) + ((0. R) * a) = ((0. R) * a) + (0. R) by RLVECT_1:def_4;
hence (0. R) * a = 0. R by ALGSTR_0:def_3; ::_thesis: verum
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
let R be non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr ; ::_thesis: for a being Element of R holds a * (0. R) = 0. R
let a be Element of R; ::_thesis: a * (0. R) = 0. R
a * (0. R) = a * ((0. R) + (0. R)) by ALGSTR_1:def_2
.= (a * (0. R)) + (a * (0. R)) by VECTSP_1:def_2 ;
then (a * (0. R)) + (a * (0. R)) = (0. R) + (a * (0. R)) by ALGSTR_1:def_2;
hence a * (0. R) = 0. R by ALGSTR_0:def_4; ::_thesis: verum
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
let V be non empty left_zeroed addLoopStr ; ::_thesis: for a being Element of V holds Sum <*a*> = a
let v be Element of V; ::_thesis: Sum <*v*> = v
reconsider a = v as Element of V ;
set S = <*v*>;
consider f being Function of NAT, the carrier of V such that
A1: Sum <*v*> = f . (len <*v*>) and
A2: ( f . 0 = 0. V & ( for j being Element of NAT
for v being Element of V st j < len <*v*> & v = <*v*> . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) by RLVECT_1:def_12;
A3: len <*a*> = 1 by FINSEQ_1:39;
0 < 1 ;
then consider j being Element of NAT such that
A4: j < len <*v*> ;
A5: <*v*> . (j + 1) = <*v*> . (0 + 1) by A3, A4, NAT_1:14
.= v by FINSEQ_1:40 ;
j = 0 by A3, A4, NAT_1:14;
then f . 1 = (0. V) + v by A2, A5
.= a by ALGSTR_1:def_2 ;
hence Sum <*v*> = v by A1, FINSEQ_1:39; ::_thesis: verum
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
let R be non empty right_add-cancelable left_zeroed right-distributive doubleLoopStr ; ::_thesis: for a being Element of R
for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)
let a be Element of R; ::_thesis: for p being FinSequence of the carrier of R holds Sum (a * p) = a * (Sum p)
let p be FinSequence of the carrier of R; ::_thesis: Sum (a * p) = a * (Sum p)
consider f being Function of NAT, the carrier of R such that
A1: Sum p = f . (len p) and
A2: f . 0 = 0. R and
A3: for j being Element of NAT
for v being Element of R st j < len p & v = p . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def_12;
consider fa being Function of NAT, the carrier of R such that
A4: Sum (a * p) = fa . (len (a * p)) and
A5: fa . 0 = 0. R and
A6: for j being Element of NAT
for v being Element of R st j < len (a * p) & v = (a * p) . (j + 1) holds
fa . (j + 1) = (fa . j) + v by RLVECT_1:def_12;
defpred S1[ Element of NAT ] means a * (f . $1) = fa . $1;
A7: Seg (len (a * p)) = dom (a * p) by FINSEQ_1:def_3
.= dom p by POLYNOM1:def_1
.= Seg (len p) by FINSEQ_1:def_3 ;
A8: now__::_thesis:_for_j_being_Element_of_NAT_st_0_<=_j_&_j_<_len_p_&_S1[j]_holds_
S1[j_+_1]
let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )
assume that
0 <= j and
A9: j < len p ; ::_thesis: ( S1[j] implies S1[j + 1] )
thus ( S1[j] implies S1[j + 1] ) ::_thesis: verum
proof
A10: 0 + 1 <= j + 1 by XREAL_1:6;
A11: j < len (a * p) by A7, A9, FINSEQ_1:6;
then j + 1 <= len (a * p) by NAT_1:13;
then j + 1 in Seg (len (a * p)) by A10, FINSEQ_1:1;
then j + 1 in dom (a * p) by FINSEQ_1:def_3;
then A12: (a * p) /. (j + 1) = (a * p) . (j + 1) by PARTFUN1:def_6;
j + 1 <= len p by A9, NAT_1:13;
then j + 1 in Seg (len p) by A10, FINSEQ_1:1;
then A13: j + 1 in dom p by FINSEQ_1:def_3;
then A14: p /. (j + 1) = p . (j + 1) by PARTFUN1:def_6;
assume S1[j] ; ::_thesis: S1[j + 1]
hence fa . (j + 1) = (a * (f . j)) + ((a * p) /. (j + 1)) by A6, A11, A12
.= (a * (f . j)) + (a * (p /. (j + 1))) by A13, POLYNOM1:def_1
.= a * ((f . j) + (p /. (j + 1))) by VECTSP_1:def_2
.= a * (f . (j + 1)) by A3, A9, A14 ;
::_thesis: verum
end;
end;
A15: S1[ 0 ] by A2, A5, Th2;
A16: for i being Element of NAT st 0 <= i & i <= len p holds
S1[i] from INT_1:sch_7(A15, A8);
thus Sum (a * p) = fa . (len p) by A4, A7, FINSEQ_1:6
.= a * (Sum p) by A1, A16 ; ::_thesis: verum
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
let R be non empty left_add-cancelable left-distributive right_zeroed doubleLoopStr ; ::_thesis: for a being Element of R
for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a
let a be Element of R; ::_thesis: for p being FinSequence of the carrier of R holds Sum (p * a) = (Sum p) * a
let p be FinSequence of the carrier of R; ::_thesis: Sum (p * a) = (Sum p) * a
consider f being Function of NAT, the carrier of R such that
A1: Sum p = f . (len p) and
A2: f . 0 = 0. R and
A3: for j being Element of NAT
for v being Element of R st j < len p & v = p . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def_12;
consider fa being Function of NAT, the carrier of R such that
A4: Sum (p * a) = fa . (len (p * a)) and
A5: fa . 0 = 0. R and
A6: for j being Element of NAT
for v being Element of R st j < len (p * a) & v = (p * a) . (j + 1) holds
fa . (j + 1) = (fa . j) + v by RLVECT_1:def_12;
defpred S1[ Element of NAT ] means (f . $1) * a = fa . $1;
A7: Seg (len (p * a)) = dom (p * a) by FINSEQ_1:def_3
.= dom p by POLYNOM1:def_2
.= Seg (len p) by FINSEQ_1:def_3 ;
A8: now__::_thesis:_for_j_being_Element_of_NAT_st_0_<=_j_&_j_<_len_p_&_S1[j]_holds_
S1[j_+_1]
let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )
assume that
0 <= j and
A9: j < len p ; ::_thesis: ( S1[j] implies S1[j + 1] )
thus ( S1[j] implies S1[j + 1] ) ::_thesis: verum
proof
A10: j < len (p * a) by A7, A9, FINSEQ_1:6;
then A11: j + 1 <= len (p * a) by NAT_1:13;
A12: 0 + 1 <= j + 1 by XREAL_1:6;
then j + 1 in Seg (len (p * a)) by A11, FINSEQ_1:1;
then j + 1 in dom (p * a) by FINSEQ_1:def_3;
then A13: (p * a) /. (j + 1) = (p * a) . (j + 1) by PARTFUN1:def_6;
j + 1 in Seg (len p) by A7, A11, A12, FINSEQ_1:1;
then A14: j + 1 in dom p by FINSEQ_1:def_3;
then A15: p /. (j + 1) = p . (j + 1) by PARTFUN1:def_6;
assume (f . j) * a = fa . j ; ::_thesis: S1[j + 1]
hence fa . (j + 1) = ((f . j) * a) + ((p * a) /. (j + 1)) by A6, A10, A13
.= ((f . j) * a) + ((p /. (j + 1)) * a) by A14, POLYNOM1:def_2
.= ((f . j) + (p /. (j + 1))) * a by VECTSP_1:def_3
.= (f . (j + 1)) * a by A3, A9, A15 ;
::_thesis: verum
end;
end;
A16: S1[ 0 ] by A2, A5, Th1;
A17: for i being Element of NAT st 0 <= i & i <= len p holds
S1[i] from INT_1:sch_7(A16, A8);
thus Sum (p * a) = fa . (len p) by A4, A7, FINSEQ_1:6
.= (Sum p) * a by A1, A17 ; ::_thesis: verum
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
let R be non empty commutative multMagma ; ::_thesis: for a being Element of R
for p being FinSequence of the carrier of R holds p * a = a * p
let a be Element of R; ::_thesis: for p being FinSequence of the carrier of R holds p * a = a * p
let p be FinSequence of the carrier of R; ::_thesis: p * a = a * p
set pa = p * a;
set ap = a * p;
A1: dom (p * a) = dom p by POLYNOM1:def_2;
A2: dom (a * p) = dom p by POLYNOM1:def_1;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(p_*_a)_holds_
(p_*_a)_/._i_=_(a_*_p)_/._i
let i be Nat; ::_thesis: ( i in dom (p * a) implies (p * a) /. i = (a * p) /. i )
assume A3: i in dom (p * a) ; ::_thesis: (p * a) /. i = (a * p) /. i
thus (p * a) /. i = (p /. i) * a by A1, A3, POLYNOM1:def_2
.= (a * p) /. i by A1, A3, POLYNOM1:def_1 ; ::_thesis: verum
end;
hence p * a = a * p by A1, A2, FINSEQ_5:12; ::_thesis: verum
end;
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 & ( 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
defpred S1[ Element of NAT , Element of R] means $2 = (p /. $1) + (q /. $1);
A1: for k being Element of NAT st k in Seg (len p) holds
ex x being Element of R st S1[k,x] ;
consider f being FinSequence of the carrier of R such that
A2: ( dom f = Seg (len p) & ( for k being Element of NAT st k in Seg (len p) holds
S1[k,f /. k] ) ) from RECDEF_1:sch_17(A1);
take f ; ::_thesis: ( dom f = dom p & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = (p /. i) + (q /. i) ) )
A3: len f = len p by A2, FINSEQ_1:def_3;
now__::_thesis:_for_m_being_Nat_st_1_<=_m_&_m_<=_len_f_holds_
f_/._m_=_(p_/._m)_+_(q_/._m)
let m be Nat; ::_thesis: ( 1 <= m & m <= len f implies f /. m = (p /. m) + (q /. m) )
assume ( 1 <= m & m <= len f ) ; ::_thesis: f /. m = (p /. m) + (q /. m)
then m in Seg (len p) by A3, FINSEQ_1:1;
hence f /. m = (p /. m) + (q /. m) by A2; ::_thesis: verum
end;
hence ( dom f = dom p & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = (p /. i) + (q /. i) ) ) by A2, FINSEQ_1:def_3; ::_thesis: verum
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
let y1, y2 be FinSequence of the carrier of R; ::_thesis: ( dom y1 = dom p & ( for i being Nat st 1 <= i & i <= len y1 holds
y1 /. i = (p /. i) + (q /. i) ) & dom y2 = dom p & ( for i being Nat st 1 <= i & i <= len y2 holds
y2 /. i = (p /. i) + (q /. i) ) implies y1 = y2 )
assume that
A4: dom y1 = dom p and
A5: for i being Nat st 1 <= i & i <= len y1 holds
y1 /. i = (p /. i) + (q /. i) and
A6: dom y2 = dom p and
A7: for i being Nat st 1 <= i & i <= len y2 holds
y2 /. i = (p /. i) + (q /. i) ; ::_thesis: y1 = y2
A8: Seg (len y1) = dom y2 by A4, A6, FINSEQ_1:def_3
.= Seg (len y2) by FINSEQ_1:def_3 ;
then A9: len y1 = len y2 by FINSEQ_1:6;
now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_<=_len_y1_holds_
y1_._i_=_y2_._i
let i be Nat; ::_thesis: ( 1 <= i & i <= len y1 implies y1 . i = y2 . i )
assume A10: ( 1 <= i & i <= len y1 ) ; ::_thesis: y1 . i = y2 . i
then i in Seg (len y2) by A8, FINSEQ_1:1;
then A11: i in dom y2 by FINSEQ_1:def_3;
i in Seg (len y1) by A10, FINSEQ_1:1;
then i in dom y1 by FINSEQ_1:def_3;
hence y1 . i = y1 /. i by PARTFUN1:def_6
.= (p /. i) + (q /. i) by A5, A10
.= y2 /. i by A7, A9, A10
.= y2 . i by A11, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence y1 = y2 by A8, FINSEQ_1:6, FINSEQ_1:14; ::_thesis: verum
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
let R be non empty Abelian add-associative right_zeroed addLoopStr ; ::_thesis: for p, q being FinSequence of the carrier of R st dom p = dom q holds
Sum (p + q) = (Sum p) + (Sum q)
let p, q be FinSequence of the carrier of R; ::_thesis: ( dom p = dom q implies Sum (p + q) = (Sum p) + (Sum q) )
consider fp being Function of NAT, the carrier of R such that
A1: Sum p = fp . (len p) and
A2: fp . 0 = 0. R and
A3: for j being Element of NAT
for v being Element of R st j < len p & v = p . (j + 1) holds
fp . (j + 1) = (fp . j) + v by RLVECT_1:def_12;
consider fq being Function of NAT, the carrier of R such that
A4: Sum q = fq . (len q) and
A5: fq . 0 = 0. R and
A6: for j being Element of NAT
for v being Element of R st j < len q & v = q . (j + 1) holds
fq . (j + 1) = (fq . j) + v by RLVECT_1:def_12;
assume dom p = dom q ; ::_thesis: Sum (p + q) = (Sum p) + (Sum q)
then A7: Seg (len p) = dom q by FINSEQ_1:def_3
.= Seg (len q) by FINSEQ_1:def_3 ;
then A8: len q = len p by FINSEQ_1:6;
consider fa being Function of NAT, the carrier of R such that
A9: Sum (p + q) = fa . (len (p + q)) and
A10: fa . 0 = 0. R and
A11: for j being Element of NAT
for v being Element of R st j < len (p + q) & v = (p + q) . (j + 1) holds
fa . (j + 1) = (fa . j) + v by RLVECT_1:def_12;
defpred S1[ Element of NAT ] means (fp . $1) + (fq . $1) = fa . $1;
A12: Seg (len p) = dom p by FINSEQ_1:def_3
.= dom (p + q) by Def1
.= Seg (len (p + q)) by FINSEQ_1:def_3 ;
then A13: len (p + q) = len p by FINSEQ_1:6;
A14: now__::_thesis:_for_j_being_Element_of_NAT_st_0_<=_j_&_j_<_len_p_&_S1[j]_holds_
S1[j_+_1]
let j be Element of NAT ; ::_thesis: ( 0 <= j & j < len p & S1[j] implies S1[j + 1] )
assume that
0 <= j and
A15: j < len p ; ::_thesis: ( S1[j] implies S1[j + 1] )
thus ( S1[j] implies S1[j + 1] ) ::_thesis: verum
proof
assume A16: S1[j] ; ::_thesis: S1[j + 1]
A17: 0 + 1 <= j + 1 by XREAL_1:6;
A18: j + 1 <= len p by A15, NAT_1:13;
then j + 1 in Seg (len p) by A17, FINSEQ_1:1;
then j + 1 in dom p by FINSEQ_1:def_3;
then A19: p /. (j + 1) = p . (j + 1) by PARTFUN1:def_6;
j + 1 in Seg (len q) by A7, A18, A17, FINSEQ_1:1;
then j + 1 in dom q by FINSEQ_1:def_3;
then A20: q /. (j + 1) = q . (j + 1) by PARTFUN1:def_6;
A21: j + 1 <= len (p + q) by A13, A15, NAT_1:13;
then j + 1 in Seg (len (p + q)) by A17, FINSEQ_1:1;
then j + 1 in dom (p + q) by FINSEQ_1:def_3;
then (p + q) /. (j + 1) = (p + q) . (j + 1) by PARTFUN1:def_6;
then fa . (j + 1) = (fa . j) + ((p + q) /. (j + 1)) by A13, A11, A15
.= ((fp . j) + (fq . j)) + ((p /. (j + 1)) + (q /. (j + 1))) by A16, A21, A17, Def1
.= (fp . j) + ((fq . j) + ((p /. (j + 1)) + (q /. (j + 1)))) by RLVECT_1:def_3
.= (fp . j) + ((p /. (j + 1)) + ((fq . j) + (q /. (j + 1)))) by RLVECT_1:def_3
.= ((fp . j) + (p /. (j + 1))) + ((fq . j) + (q /. (j + 1))) by RLVECT_1:def_3
.= (fp . (j + 1)) + ((fq . j) + (q /. (j + 1))) by A3, A15, A19
.= (fp . (j + 1)) + (fq . (j + 1)) by A8, A6, A15, A20 ;
hence S1[j + 1] ; ::_thesis: verum
end;
end;
A22: S1[ 0 ] by A2, A5, A10, RLVECT_1:def_4;
A23: for i being Element of NAT st 0 <= i & i <= len p holds
S1[i] from INT_1:sch_7(A22, A14);
thus Sum (p + q) = fa . (len p) by A12, A9, FINSEQ_1:6
.= (Sum p) + (Sum q) by A8, A1, A4, A23 ; ::_thesis: verum
end;
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
proof
reconsider n = n as Element of NAT by ORDINAL1:def_12;
(power R) . (a,n) is Element of R ;
hence (power R) . (a,n) is Element of R ; ::_thesis: verum
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
let R be non empty unital multMagma ; ::_thesis: for a being Element of R holds
( a |^ 0 = 1_ R & a |^ 1 = a )
let a be Element of R; ::_thesis: ( a |^ 0 = 1_ R & a |^ 1 = a )
thus a |^ 0 = 1_ R by GROUP_1:def_7; ::_thesis: a |^ 1 = a
0 + 1 = 1 ;
then (power R) . (a,1) = ((power R) . (a,0)) * a by GROUP_1:def_7
.= (1_ R) * a by GROUP_1:def_7
.= a by GROUP_1:def_4 ;
hence a |^ 1 = a ; ::_thesis: verum
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
let R be non empty unital associative commutative multMagma ; ::_thesis: for a, b being Element of R
for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)
let a, b be Element of R; ::_thesis: for n being Nat holds (a * b) |^ n = (a |^ n) * (b |^ n)
let n be Nat; ::_thesis: (a * b) |^ n = (a |^ n) * (b |^ n)
A1: n in NAT by ORDINAL1:def_12;
defpred S1[ Element of NAT ] means (power R) . ((a * b),$1) = ((power R) . (a,$1)) * ((power R) . (b,$1));
A2: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume S1[m] ; ::_thesis: S1[m + 1]
then (power R) . ((a * b),(m + 1)) = (((power R) . (a,m)) * ((power R) . (b,m))) * (a * b) by GROUP_1:def_7
.= ((((power R) . (a,m)) * ((power R) . (b,m))) * a) * b by GROUP_1:def_3
.= ((((power R) . (a,m)) * a) * ((power R) . (b,m))) * b by GROUP_1:def_3
.= (((power R) . (a,m)) * a) * (((power R) . (b,m)) * b) by GROUP_1:def_3
.= ((power R) . (a,(m + 1))) * (((power R) . (b,m)) * b) by GROUP_1:def_7
.= ((power R) . (a,(m + 1))) * ((power R) . (b,(m + 1))) by GROUP_1:def_7 ;
hence S1[m + 1] ; ::_thesis: verum
end;
(power R) . ((a * b),0) = 1_ R by GROUP_1:def_7
.= (1_ R) * (1_ R) by GROUP_1:def_4
.= ((power R) . (a,0)) * (1_ R) by GROUP_1:def_7
.= ((power R) . (a,0)) * ((power R) . (b,0)) by GROUP_1:def_7 ;
then A3: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A2);
hence (a * b) |^ n = (a |^ n) * (b |^ n) by A1; ::_thesis: verum
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
let R be non empty unital associative multMagma ; ::_thesis: for a being Element of R
for n, m being Element of NAT holds a |^ (n + m) = (a |^ n) * (a |^ m)
let a be Element of R; ::_thesis: for n, m being Element of NAT holds a |^ (n + m) = (a |^ n) * (a |^ m)
let n, m be Element of NAT ; ::_thesis: a |^ (n + m) = (a |^ n) * (a |^ m)
defpred S1[ Element of NAT ] means (power R) . (a,(n + $1)) = ((power R) . (a,n)) * ((power R) . (a,$1));
A1: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: S1[m] ; ::_thesis: S1[m + 1]
(power R) . (a,(n + (m + 1))) = (power R) . (a,((n + m) + 1))
.= (((power R) . (a,n)) * ((power R) . (a,m))) * a by A2, GROUP_1:def_7
.= ((power R) . (a,n)) * (((power R) . (a,m)) * a) by GROUP_1:def_3
.= ((power R) . (a,n)) * ((power R) . (a,(m + 1))) by GROUP_1:def_7 ;
hence S1[m + 1] ; ::_thesis: verum
end;
(power R) . (a,(n + 0)) = ((power R) . (a,n)) * (1_ R) by GROUP_1:def_4
.= ((power R) . (a,n)) * ((power R) . (a,0)) by GROUP_1:def_7 ;
then A3: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1);
hence a |^ (n + m) = (a |^ n) * (a |^ m) ; ::_thesis: verum
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
let R be non empty unital associative multMagma ; ::_thesis: for a being Element of R
for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)
let a be Element of R; ::_thesis: for n, m being Nat holds a |^ (n + m) = (a |^ n) * (a |^ m)
let n, m be Nat; ::_thesis: a |^ (n + m) = (a |^ n) * (a |^ m)
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def_12;
a |^ (n1 + m1) = (a |^ n1) * (a |^ m1) by Lm3;
hence a |^ (n + m) = (a |^ n) * (a |^ m) ; ::_thesis: verum
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
let R be non empty unital associative multMagma ; ::_thesis: for a being Element of R
for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)
let a be Element of R; ::_thesis: for n, m being Nat holds (a |^ n) |^ m = a |^ (n * m)
let n, m be Nat; ::_thesis: (a |^ n) |^ m = a |^ (n * m)
A1: ( n in NAT & m in NAT ) by ORDINAL1:def_12;
defpred S1[ Element of NAT ] means (power R) . ((a |^ n),$1) = (power R) . (a,(n * $1));
A2: now__::_thesis:_for_m_being_Element_of_NAT_st_S1[m]_holds_
S1[m_+_1]
let m be Element of NAT ; ::_thesis: ( S1[m] implies S1[m + 1] )
assume S1[m] ; ::_thesis: S1[m + 1]
then (power R) . ((a |^ n),(m + 1)) = (a |^ (n * m)) * (a |^ n) by GROUP_1:def_7
.= a |^ ((n * m) + n) by Th10
.= (power R) . (a,(n * (m + 1))) ;
hence S1[m + 1] ; ::_thesis: verum
end;
(power R) . ((a |^ n),0) = 1_ R by GROUP_1:def_7
.= (power R) . (a,(n * 0)) by GROUP_1:def_7 ;
then A3: S1[ 0 ] ;
for k being Element of NAT holds S1[k] from NAT_1:sch_1(A3, A2);
hence (a |^ n) |^ m = a |^ (n * m) by A1; ::_thesis: verum
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
set D = the carrier of R;
consider g being Function of [:NAT, the carrier of R:], the carrier of R such that
A1: for a being Element of the carrier of R holds
( g . (0,a) = 0. R & ( for n being Element of NAT holds g . ((n + 1),a) = the addF of R . (a,(g . (n,a))) ) ) by Lm1;
take g ; ::_thesis: for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Element of NAT holds g . ((n + 1),a) = a + (g . (n,a)) ) )
thus for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Element of NAT holds g . ((n + 1),a) = a + (g . (n,a)) ) ) by A1; ::_thesis: verum
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
let f, g be Function of [:NAT, the carrier of R:], the carrier of R; ::_thesis: ( ( for a being Element of R holds
( f . (0,a) = 0. R & ( for n being Element of NAT holds f . ((n + 1),a) = a + (f . (n,a)) ) ) ) & ( for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Element of NAT holds g . ((n + 1),a) = a + (g . (n,a)) ) ) ) implies f = g )
assume A2: for a being Element of R holds
( f . (0,a) = 0. R & ( for n being Element of NAT holds f . ((n + 1),a) = a + (f . (n,a)) ) ) ; ::_thesis: ( ex a being Element of R st
( g . (0,a) = 0. R implies ex n being Element of NAT st not g . ((n + 1),a) = a + (g . (n,a)) ) or f = g )
defpred S1[ Element of NAT ] means for a being Element of R holds f . ($1,a) = g . ($1,a);
assume A3: for a being Element of R holds
( g . (0,a) = 0. R & ( for n being Element of NAT holds g . ((n + 1),a) = a + (g . (n,a)) ) ) ; ::_thesis: f = g
A4: 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 A5: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_a_being_Element_of_R_holds_f_._((n_+_1),a)_=_g_._((n_+_1),a)
let a be Element of R; ::_thesis: f . ((n + 1),a) = g . ((n + 1),a)
thus f . ((n + 1),a) = a + (f . (n,a)) by A2
.= a + (g . (n,a)) by A5
.= g . ((n + 1),a) by A3 ; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A6: S1[ 0 ]
proof
let a be Element of R; ::_thesis: f . (0,a) = g . (0,a)
thus f . (0,a) = 0. R by A2
.= g . (0,a) by A3 ; ::_thesis: verum
end;
A7: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A6, A4);
A8: now__::_thesis:_for_x_being_set_st_x_in_[:NAT,_the_carrier_of_R:]_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in [:NAT, the carrier of R:] implies f . x = g . x )
assume x in [:NAT, the carrier of R:] ; ::_thesis: f . x = g . x
then consider u, v being set such that
A9: u in NAT and
A10: v in the carrier of R and
A11: x = [u,v] by ZFMISC_1:def_2;
reconsider v = v as Element of R by A10;
reconsider u = u as Element of NAT by A9;
thus f . x = f . (u,v) by A11
.= g . (u,v) by A7
.= g . x by A11 ; ::_thesis: verum
end;
( dom f = [:NAT, the carrier of R:] & dom g = [:NAT, the carrier of R:] ) by FUNCT_2:def_1;
hence f = g by A8, FUNCT_1:2; ::_thesis: verum
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
consider g being Function of [: the carrier of R,NAT:], the carrier of R such that
A12: for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = the addF of R . ((g . (a,n)),a) ) ) by Lm2;
take g ; ::_thesis: for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) )
thus for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) ) by A12; ::_thesis: verum
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
let f, g be Function of [: the carrier of R,NAT:], the carrier of R; ::_thesis: ( ( for a being Element of R holds
( f . (a,0) = 0. R & ( for n being Element of NAT holds f . (a,(n + 1)) = (f . (a,n)) + a ) ) ) & ( for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) ) ) implies f = g )
assume A13: for a being Element of R holds
( f . (a,0) = 0. R & ( for n being Element of NAT holds f . (a,(n + 1)) = (f . (a,n)) + a ) ) ; ::_thesis: ( ex a being Element of R st
( g . (a,0) = 0. R implies ex n being Element of NAT st not g . (a,(n + 1)) = (g . (a,n)) + a ) or f = g )
defpred S1[ Element of NAT ] means for a being Element of R holds f . (a,$1) = g . (a,$1);
assume A14: for a being Element of R holds
( g . (a,0) = 0. R & ( for n being Element of NAT holds g . (a,(n + 1)) = (g . (a,n)) + a ) ) ; ::_thesis: f = g
A15: 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 A16: S1[n] ; ::_thesis: S1[n + 1]
now__::_thesis:_for_a_being_Element_of_R_holds_f_._(a,(n_+_1))_=_g_._(a,(n_+_1))
let a be Element of R; ::_thesis: f . (a,(n + 1)) = g . (a,(n + 1))
thus f . (a,(n + 1)) = (f . (a,n)) + a by A13
.= (g . (a,n)) + a by A16
.= g . (a,(n + 1)) by A14 ; ::_thesis: verum
end;
hence S1[n + 1] ; ::_thesis: verum
end;
A17: S1[ 0 ]
proof
let a be Element of R; ::_thesis: f . (a,0) = g . (a,0)
thus f . (a,0) = 0. R by A13
.= g . (a,0) by A14 ; ::_thesis: verum
end;
A18: for n being Element of NAT holds S1[n] from NAT_1:sch_1(A17, A15);
A19: now__::_thesis:_for_x_being_set_st_x_in_[:_the_carrier_of_R,NAT:]_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in [: the carrier of R,NAT:] implies f . x = g . x )
assume x in [: the carrier of R,NAT:] ; ::_thesis: f . x = g . x
then consider v, u being set such that
A20: v in the carrier of R and
A21: u in NAT and
A22: x = [v,u] by ZFMISC_1:def_2;
reconsider v = v as Element of R by A20;
reconsider u = u as Element of NAT by A21;
thus f . x = f . (v,u) by A22
.= g . (v,u) by A18
.= g . x by A22 ; ::_thesis: verum
end;
( dom f = [: the carrier of R,NAT:] & dom g = [: the carrier of R,NAT:] ) by FUNCT_2:def_1;
hence f = g by A19, FUNCT_1:2; ::_thesis: verum
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 ;
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 & 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
let R be non empty right_zeroed addLoopStr ; ::_thesis: for a being Element of R holds 1 * a = a
let a be Element of R; ::_thesis: 1 * a = a
thus 1 * a = (Nat-mult-left R) . ((0 + 1),a)
.= a + ((Nat-mult-left R) . (0,a)) by Def3
.= a + (0. R) by Def3
.= a by RLVECT_1:def_4 ; ::_thesis: verum
end;
theorem Th14: :: BINOM:14
for R being non empty left_zeroed addLoopStr
for a being Element of R holds a * 1 = a
proof
let R be non empty left_zeroed addLoopStr ; ::_thesis: for a being Element of R holds a * 1 = a
let a be Element of R; ::_thesis: a * 1 = a
thus a * 1 = (Nat-mult-right R) . (a,(0 + 1))
.= ((Nat-mult-right R) . (a,0)) + a by Def4
.= (0. R) + a by Def4
.= a by ALGSTR_1:def_2 ; ::_thesis: verum
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
let R be non empty left_zeroed add-associative addLoopStr ; ::_thesis: for a being Element of R
for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)
let a be Element of R; ::_thesis: for n, m being Element of NAT holds (n + m) * a = (n * a) + (m * a)
let n, m be Element of NAT ; ::_thesis: (n + m) * a = (n * a) + (m * a)
defpred S1[ Element of NAT ] means ($1 + m) * a = ($1 * a) + (m * a);
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
((k + 1) + m) * a = ((k + m) + 1) * a
.= a + ((k * a) + (m * a)) by A2, Def3
.= (a + (k * a)) + (m * a) by RLVECT_1:def_3
.= ((k + 1) * a) + (m * a) by Def3 ;
hence S1[k + 1] ; ::_thesis: verum
end;
(0 + m) * a = (0. R) + (m * a) by ALGSTR_1:def_2
.= (0 * a) + (m * a) by Def3 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence (n + m) * a = (n * a) + (m * a) ; ::_thesis: verum
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
let R be non empty add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of R
for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)
let a be Element of R; ::_thesis: for n, m being Element of NAT holds a * (n + m) = (a * n) + (a * m)
let n, m be Element of NAT ; ::_thesis: a * (n + m) = (a * n) + (a * m)
defpred S1[ Element of NAT ] means a * (n + $1) = (a * n) + (a * $1);
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
a * (n + (k + 1)) = a * ((n + k) + 1)
.= ((a * n) + (a * k)) + a by A2, Def4
.= (a * n) + ((a * k) + a) by RLVECT_1:def_3
.= (a * n) + (a * (k + 1)) by Def4 ;
hence S1[k + 1] ; ::_thesis: verum
end;
a * (n + 0) = (a * n) + (0. R) by RLVECT_1:def_4
.= (a * n) + (a * 0) by Def4 ;
then A3: S1[ 0 ] ;
for m being Element of NAT holds S1[m] from NAT_1:sch_1(A3, A1);
hence a * (n + m) = (a * n) + (a * m) ; ::_thesis: verum
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
let R be non empty left_zeroed add-associative right_zeroed addLoopStr ; ::_thesis: for a being Element of R
for n being Element of NAT holds n * a = a * n
let a be Element of R; ::_thesis: for n being Element of NAT holds n * a = a * n
let n be Element of NAT ; ::_thesis: n * a = a * n
defpred S1[ Element of NAT ] means $1 * a = a * $1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
(k + 1) * a = (k * a) + (1 * a) by Th15
.= (k * a) + a by Th13
.= (a * k) + (a * 1) by A2, Th14
.= a * (k + 1) by Th16 ;
hence S1[k + 1] ; ::_thesis: verum
end;
0 * a = 0. R by Def3
.= a * 0 by Def4 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence n * a = a * n ; ::_thesis: verum
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
let R be non empty Abelian addLoopStr ; ::_thesis: for a being Element of R
for n being Element of NAT holds n * a = a * n
let a be Element of R; ::_thesis: for n being Element of NAT holds n * a = a * n
let n be Element of NAT ; ::_thesis: n * a = a * n
defpred S1[ Element of NAT ] means $1 * a = a * $1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then (k + 1) * a = a + (a * k) by Def3
.= a * (k + 1) by Def4 ;
hence S1[k + 1] ; ::_thesis: verum
end;
0 * a = 0. R by Def3
.= a * 0 by Def4 ;
then A2: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A2, A1);
hence n * a = a * n ; ::_thesis: verum
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
let R be non empty left_add-cancelable left_zeroed left-distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds (n * a) * b = n * (a * b)
let a, b be Element of R; ::_thesis: for n being Element of NAT holds (n * a) * b = n * (a * b)
let n be Element of NAT ; ::_thesis: (n * a) * b = n * (a * b)
defpred S1[ Element of NAT ] means ($1 * a) * b = $1 * (a * b);
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
((k + 1) * a) * b = (a + (k * a)) * b by Def3
.= (a * b) + (k * (a * b)) by A2, VECTSP_1:def_3
.= (1 * (a * b)) + (k * (a * b)) by Th13
.= (k + 1) * (a * b) by Th15 ;
hence S1[k + 1] ; ::_thesis: verum
end;
(0 * a) * b = (0. R) * b by Def3
.= 0. R by Th1
.= 0 * (a * b) by Def3 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence (n * a) * b = n * (a * b) ; ::_thesis: verum
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
let R be non empty right_add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds b * (n * a) = (b * a) * n
let a, b be Element of R; ::_thesis: for n being Element of NAT holds b * (n * a) = (b * a) * n
let n be Element of NAT ; ::_thesis: b * (n * a) = (b * a) * n
defpred S1[ Element of NAT ] means b * ($1 * a) = (b * a) * $1;
A1: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_
S1[k_+_1]
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; ::_thesis: S1[k + 1]
b * ((k + 1) * a) = b * (a + (k * a)) by Def3
.= (b * a) + ((b * a) * k) by A2, VECTSP_1:def_2
.= ((b * a) * 1) + ((b * a) * k) by Th14
.= (b * a) * (k + 1) by Th16 ;
hence S1[k + 1] ; ::_thesis: verum
end;
b * (0 * a) = b * (0. R) by Def3
.= 0. R by Th2
.= (b * a) * 0 by Def4 ;
then A3: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence b * (n * a) = (b * a) * n ; ::_thesis: verum
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
let R be non empty add-cancelable left_zeroed distributive add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds (a * n) * b = a * (n * b)
let a, b be Element of R; ::_thesis: for n being Element of NAT holds (a * n) * b = a * (n * b)
let n be Element of NAT ; ::_thesis: (a * n) * b = a * (n * b)
thus (a * n) * b = (n * a) * b by Th17
.= n * (a * b) by Th19
.= (a * b) * n by Th17
.= a * (n * b) by Th20 ; ::_thesis: verum
end;
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 & ( 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
defpred S1[ Element of NAT , Element of R] means for l, m being Element of NAT st m = $1 - 1 & l = n - m holds
$2 = ((n choose m) * (a |^ l)) * (b |^ m);
A1: for k being Element of NAT st k in Seg (n + 1) holds
ex y being Element of R st S1[k,y]
proof
let k be Element of NAT ; ::_thesis: ( k in Seg (n + 1) implies ex y being Element of R st S1[k,y] )
assume A2: k in Seg (n + 1) ; ::_thesis: ex y being Element of R st S1[k,y]
then k >= 1 by FINSEQ_1:1;
then reconsider m1 = k - 1 as Element of NAT by INT_1:5;
k <= n + 1 by A2, FINSEQ_1:1;
then k - 1 <= (n + 1) - 1 by XREAL_1:9;
then reconsider l1 = n - m1 as Element of NAT by INT_1:5;
reconsider z = ((n choose m1) * (a |^ l1)) * (b |^ m1) as Element of R ;
take z ; ::_thesis: S1[k,z]
thus S1[k,z] ; ::_thesis: verum
end;
consider p being FinSequence of the carrier of R such that
A3: ( dom p = Seg (n + 1) & ( for k being Element of NAT st k in Seg (n + 1) holds
S1[k,p /. k] ) ) from RECDEF_1:sch_17(A1);
take p ; ::_thesis: ( len p = n + 1 & ( for i, l, m being Element of NAT st i in dom p & m = i - 1 & l = n - m holds
p /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) )
thus ( len p = n + 1 & ( for i, l, m being Element of NAT st i in dom p & m = i - 1 & l = n - m holds
p /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) ) by A3, FINSEQ_1:def_3; ::_thesis: verum
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
let f, g be FinSequence of the carrier of R; ::_thesis: ( len f = n + 1 & ( for i, l, m being Element of NAT st i in dom f & m = i - 1 & l = n - m holds
f /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) & len g = n + 1 & ( for i, l, m being Element of NAT st i in dom g & m = i - 1 & l = n - m holds
g /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) implies f = g )
assume that
A4: len f = n + 1 and
A5: for i, l, m being Element of NAT st i in dom f & m = i - 1 & l = n - m holds
f /. i = ((n choose m) * (a |^ l)) * (b |^ m) ; ::_thesis: ( not len g = n + 1 or ex i, l, m being Element of NAT st
( i in dom g & m = i - 1 & l = n - m & not g /. i = ((n choose m) * (a |^ l)) * (b |^ m) ) or f = g )
assume that
A6: len g = n + 1 and
A7: for i, l, m being Element of NAT st i in dom g & m = i - 1 & l = n - m holds
g /. i = ((n choose m) * (a |^ l)) * (b |^ m) ; ::_thesis: f = g
for i being Nat st 1 <= i & i <= len f holds
f . i = g . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len f implies f . i = g . i )
assume that
A8: 1 <= i and
A9: i <= len f ; ::_thesis: f . i = g . i
reconsider m = i - 1 as Element of NAT by A8, INT_1:5;
i - 1 <= (n + 1) - 1 by A4, A9, XREAL_1:9;
then reconsider l = n - m as Element of NAT by INT_1:5;
A10: i in Seg (n + 1) by A4, A8, A9, FINSEQ_1:1;
then A11: i in dom f by A4, FINSEQ_1:def_3;
A12: i in dom g by A6, A10, FINSEQ_1:def_3;
hence g . i = g /. i by PARTFUN1:def_6
.= ((n choose m) * (a |^ l)) * (b |^ m) by A7, A12
.= f /. i by A5, A11
.= f . i by A11, PARTFUN1:def_6 ;
::_thesis: verum
end;
hence f = g by A4, A6, FINSEQ_1:14; ::_thesis: verum
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
let R be non empty unital right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R holds (a,b) In_Power 0 = <*(1_ R)*>
let a, b be Element of R; ::_thesis: (a,b) In_Power 0 = <*(1_ R)*>
set p = (a,b) In_Power 0;
A1: len ((a,b) In_Power 0) = 0 + 1 by Def7
.= 1 ;
then A2: dom ((a,b) In_Power 0) = {1} by FINSEQ_1:2, FINSEQ_1:def_3;
then A3: 1 in dom ((a,b) In_Power 0) by TARSKI:def_1;
then consider i being Element of NAT such that
A4: i in dom ((a,b) In_Power 0) ;
A5: i = 1 by A2, A4, TARSKI:def_1;
then reconsider m = i - 1 as Element of NAT by INT_1:5;
reconsider l = 0 - m as Element of NAT by A5;
((a,b) In_Power 0) . 1 = ((a,b) In_Power 0) /. 1 by A3, PARTFUN1:def_6
.= ((0 choose m) * (a |^ l)) * (b |^ m) by A3, A5, Def7
.= (1 * (a |^ l)) * (b |^ m) by A5, NEWTON:19
.= (1 * (a |^ 0)) * (1_ R) by A5, Th8
.= (1 * (1_ R)) * (1_ R) by Th8
.= (1_ R) * (1_ R) by Th13
.= 1_ R by GROUP_1:def_4 ;
hence (a,b) In_Power 0 = <*(1_ R)*> by A1, FINSEQ_1:40; ::_thesis: verum
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
reconsider m = 1 - 1 as Element of NAT by NEWTON:19;
let R be non empty unital right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds ((a,b) In_Power n) . 1 = a |^ n
let a, b be Element of R; ::_thesis: for n being Element of NAT holds ((a,b) In_Power n) . 1 = a |^ n
let n be Element of NAT ; ::_thesis: ((a,b) In_Power n) . 1 = a |^ n
reconsider l = n - m as Element of NAT ;
len ((a,b) In_Power n) = n + 1 by Def7;
then A1: dom ((a,b) In_Power n) = Seg (n + 1) by FINSEQ_1:def_3;
0 + 1 <= n + 1 by XREAL_1:6;
then A2: 1 in dom ((a,b) In_Power n) by A1, FINSEQ_1:1;
hence ((a,b) In_Power n) . 1 = ((a,b) In_Power n) /. 1 by PARTFUN1:def_6
.= ((n choose 0) * (a |^ l)) * (b |^ m) by A2, Def7
.= (1 * (a |^ n)) * (b |^ 0) by NEWTON:19
.= (a |^ n) * (b |^ 0) by Th13
.= (a |^ n) * (1_ R) by Th8
.= a |^ n by GROUP_1:def_4 ;
::_thesis: verum
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
let R be non empty unital right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds ((a,b) In_Power n) . (n + 1) = b |^ n
let a, b be Element of R; ::_thesis: for n being Element of NAT holds ((a,b) In_Power n) . (n + 1) = b |^ n
let n be Element of NAT ; ::_thesis: ((a,b) In_Power n) . (n + 1) = b |^ n
reconsider m = (n + 1) - 1 as Element of NAT ;
reconsider l = n - m as Element of NAT by INT_1:5;
len ((a,b) In_Power n) = n + 1 by Def7;
then A1: dom ((a,b) In_Power n) = Seg (n + 1) by FINSEQ_1:def_3;
then A2: ( l = 0 & n + 1 in dom ((a,b) In_Power n) ) by FINSEQ_1:4;
thus ((a,b) In_Power n) . (n + 1) = ((a,b) In_Power n) /. (n + 1) by A1, FINSEQ_1:4, PARTFUN1:def_6
.= ((n choose n) * (a |^ 0)) * (b |^ n) by A2, Def7
.= (1 * (a |^ 0)) * (b |^ n) by NEWTON:21
.= (1 * (1_ R)) * (b |^ n) by Th8
.= (1_ R) * (b |^ n) by Th13
.= b |^ n by GROUP_1:def_4 ; ::_thesis: verum
end;
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
let R be non empty add-cancelable left_zeroed unital associative commutative distributive Abelian add-associative right_zeroed doubleLoopStr ; ::_thesis: for a, b being Element of R
for n being Element of NAT holds (a + b) |^ n = Sum ((a,b) In_Power n)
let a, b be Element of R; ::_thesis: for n being Element of NAT holds (a + b) |^ n = Sum ((a,b) In_Power n)
let n be Element of NAT ; ::_thesis: (a + b) |^ n = Sum ((a,b) In_Power n)
defpred S1[ Element of NAT ] means (a + b) |^ $1 = Sum ((a,b) In_Power $1);
A1: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
set G1 = (((a,b) In_Power n) * a) ^ <*(0. R)*>;
set G2 = <*(0. R)*> ^ (((a,b) In_Power n) * b);
A2: Seg (len (((a,b) In_Power n) * a)) = dom (((a,b) In_Power n) * a) by FINSEQ_1:def_3
.= dom ((a,b) In_Power n) by POLYNOM1:def_2
.= Seg (len ((a,b) In_Power n)) by FINSEQ_1:def_3 ;
len ((((a,b) In_Power n) * a) ^ <*(0. R)*>) = (len (((a,b) In_Power n) * a)) + (len <*(0. R)*>) by FINSEQ_1:22
.= (len (((a,b) In_Power n) * a)) + 1 by FINSEQ_1:40
.= (len ((a,b) In_Power n)) + 1 by A2, FINSEQ_1:6
.= (n + 1) + 1 by Def7 ;
then reconsider F1 = (((a,b) In_Power n) * a) ^ <*(0. R)*> as Element of ((n + 1) + 1) -tuples_on the carrier of R by FINSEQ_2:92;
A3: Seg (len (((a,b) In_Power n) * b)) = dom (((a,b) In_Power n) * b) by FINSEQ_1:def_3
.= dom ((a,b) In_Power n) by POLYNOM1:def_2
.= Seg (len ((a,b) In_Power n)) by FINSEQ_1:def_3 ;
len (<*(0. R)*> ^ (((a,b) In_Power n) * b)) = (len (((a,b) In_Power n) * b)) + (len <*(0. R)*>) by FINSEQ_1:22
.= (len (((a,b) In_Power n) * b)) + 1 by FINSEQ_1:40
.= (len ((a,b) In_Power n)) + 1 by A3, FINSEQ_1:6
.= (n + 1) + 1 by Def7 ;
then reconsider F2 = <*(0. R)*> ^ (((a,b) In_Power n) * b) as Element of ((n + 1) + 1) -tuples_on the carrier of R by FINSEQ_2:92;
A4: len F1 = (n + 1) + 1 by CARD_1:def_7;
set F = F1 + F2;
A5: len F2 = (n + 1) + 1 by CARD_1:def_7;
A6: Seg (len (F1 + F2)) = dom (F1 + F2) by FINSEQ_1:def_3
.= dom F1 by Def1
.= Seg (len F1) by FINSEQ_1:def_3 ;
then A7: len (F1 + F2) = (n + 1) + 1 by A4, FINSEQ_1:6;
A8: for i being Nat st 1 <= i & i <= len ((a,b) In_Power (n + 1)) holds
(F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
proof
let i be Nat; ::_thesis: ( 1 <= i & i <= len ((a,b) In_Power (n + 1)) implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
assume that
A9: 1 <= i and
A10: i <= len ((a,b) In_Power (n + 1)) ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
A11: len ((a,b) In_Power (n + 1)) = (n + 1) + 1 by Def7;
then A12: dom ((a,b) In_Power (n + 1)) = Seg ((n + 1) + 1) by FINSEQ_1:def_3;
then A13: i in dom ((a,b) In_Power (n + 1)) by A9, A10, A11, FINSEQ_1:1;
reconsider j = i - 1 as Element of NAT by A9, INT_1:5;
set x = ((a,b) In_Power n) /. j;
set r1 = F1 /. i;
set r2 = F2 /. i;
set r = ((a,b) In_Power n) /. i;
A14: i = j + 1 ;
A15: i in Seg ((n + 1) + 1) by A9, A10, A11, FINSEQ_1:1;
then A16: i in dom F1 by A4, FINSEQ_1:def_3;
A17: i in dom F2 by A5, A15, FINSEQ_1:def_3;
A18: i <= len (F1 + F2) by A7, A10, Def7;
A19: ( i in {((n + 1) + 1)} implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
assume A20: i in {((n + 1) + 1)} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A21: i = (n + 1) + 1 by TARSKI:def_1;
n + 1 = len ((a,b) In_Power n) by Def7
.= len (((a,b) In_Power n) * a) by A2, FINSEQ_1:6 ;
then A22: F1 /. i = ((((a,b) In_Power n) * a) ^ <*(0. R)*>) . ((len (((a,b) In_Power n) * a)) + 1) by A16, A21, PARTFUN1:def_6
.= 0. R by FINSEQ_1:42 ;
A23: j = ((n + 1) + 1) - 1 by A20, TARSKI:def_1
.= n + 1 ;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then A24: j in Seg (len ((a,b) In_Power n)) by A23, Def7;
then A25: j in dom (((a,b) In_Power n) * b) by A3, FINSEQ_1:def_3;
A26: j in dom ((a,b) In_Power n) by A24, FINSEQ_1:def_3;
then A27: ((a,b) In_Power n) /. j = ((a,b) In_Power n) . (n + 1) by A23, PARTFUN1:def_6
.= b |^ n by Th24 ;
A28: F2 /. i = (<*(0. R)*> ^ (((a,b) In_Power n) * b)) . (1 + (n + 1)) by A17, A21, PARTFUN1:def_6
.= (<*(0. R)*> ^ (((a,b) In_Power n) * b)) . ((len <*(0. R)*>) + j) by A23, FINSEQ_1:39
.= (((a,b) In_Power n) * b) . j by A25, FINSEQ_1:def_7
.= (((a,b) In_Power n) * b) /. j by A25, PARTFUN1:def_6
.= (b |^ n) * b by A26, A27, POLYNOM1:def_2
.= b |^ (n + 1) by GROUP_1:def_7 ;
dom (F1 + F2) = Seg ((n + 1) + 1) by A4, A6, FINSEQ_1:def_3;
then i in dom (F1 + F2) by A9, A21, FINSEQ_1:1;
hence (F1 + F2) . i = (F1 + F2) /. i by PARTFUN1:def_6
.= (0. R) + (F2 /. i) by A9, A18, A22, Def1
.= b |^ (n + 1) by A28, ALGSTR_1:def_2
.= ((a,b) In_Power (n + 1)) . i by A21, Th24 ;
::_thesis: verum
end;
A29: i in dom (F1 + F2) by A4, A6, A15, FINSEQ_1:def_3;
A30: ( i in { k where k is Element of NAT : ( k > 1 & k < (n + 1) + 1 ) } implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
assume i in { k where k is Element of NAT : ( 1 < k & k < (n + 1) + 1 ) } ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A31: ex k being Element of NAT st
( k = i & 1 < k & k < (n + 1) + 1 ) ;
then reconsider m1 = i - 1 as Element of NAT by INT_1:5;
A32: i <= n + 1 by A31, NAT_1:13;
then i in Seg (n + 1) by A31, FINSEQ_1:1;
then A33: i in Seg (len ((a,b) In_Power n)) by Def7;
then A34: i in dom ((a,b) In_Power n) by FINSEQ_1:def_3;
1 <= j by A14, A31, NAT_1:13;
then reconsider m2 = j - 1 as Element of NAT by INT_1:5;
A35: j <= n + 1 by A14, A31, XREAL_1:6;
then j - 1 <= (n + 1) - 1 by XREAL_1:9;
then reconsider l2 = n - m2 as Element of NAT by INT_1:5;
1 <= j by A14, A31, NAT_1:13;
then j in Seg (n + 1) by A35, FINSEQ_1:1;
then A36: j in Seg (len ((a,b) In_Power n)) by Def7;
then A37: j in dom ((a,b) In_Power n) by FINSEQ_1:def_3;
A38: j in dom (((a,b) In_Power n) * b) by A3, A36, FINSEQ_1:def_3;
A39: j in dom (((a,b) In_Power n) * b) by A3, A36, FINSEQ_1:def_3;
F2 /. i = (<*(0. R)*> ^ (((a,b) In_Power n) * b)) . i by A17, PARTFUN1:def_6;
then A40: F2 /. i = (<*(0. R)*> ^ (((a,b) In_Power n) * b)) . ((len <*(0. R)*>) + j) by A14, FINSEQ_1:40
.= (((a,b) In_Power n) * b) . j by A39, FINSEQ_1:def_7
.= (((a,b) In_Power n) * b) /. j by A38, PARTFUN1:def_6
.= (((a,b) In_Power n) /. j) * b by A37, POLYNOM1:def_2 ;
i - 1 <= (n + 1) - 1 by A32, XREAL_1:9;
then reconsider l1 = n - m1 as Element of NAT by INT_1:5;
A41: l1 + 1 = (n + 1) - (m2 + 1) ;
A42: i in dom (((a,b) In_Power n) * a) by A2, A33, FINSEQ_1:def_3;
F1 /. i = ((((a,b) In_Power n) * a) ^ <*(0. R)*>) . i by A16, PARTFUN1:def_6;
then A43: F1 /. i = (((a,b) In_Power n) * a) . i by A42, FINSEQ_1:def_7
.= (((a,b) In_Power n) * a) /. i by A42, PARTFUN1:def_6
.= (((a,b) In_Power n) /. i) * a by A34, POLYNOM1:def_2 ;
thus (F1 + F2) . i = (F1 + F2) /. i by A29, PARTFUN1:def_6
.= (F1 /. i) + ((((a,b) In_Power n) /. j) * b) by A9, A18, A40, Def1
.= ((((n choose m1) * (a |^ l1)) * (b |^ m1)) * a) + ((((a,b) In_Power n) /. j) * b) by A34, A43, Def7
.= ((((a |^ l1) * (n choose m1)) * (b |^ m1)) * a) + ((((a,b) In_Power n) /. j) * b) by Th17
.= (a * ((a |^ l1) * ((n choose m1) * (b |^ m1)))) + ((((a,b) In_Power n) /. j) * b) by Th21
.= ((a * (a |^ l1)) * ((n choose m1) * (b |^ m1))) + ((((a,b) In_Power n) /. j) * b) by GROUP_1:def_3
.= ((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + ((((a,b) In_Power n) /. j) * b) by GROUP_1:def_7
.= ((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * ((n choose m2) * (a |^ l2))) * b) by A37, Def7
.= ((a |^ (l1 + 1)) * ((n choose m1) * (b |^ m1))) + (((b |^ m2) * b) * ((n choose m2) * (a |^ l2))) by GROUP_1:def_3
.= ((a |^ (l1 + 1)) * ((n choose (m2 + 1)) * (b |^ (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2))) by GROUP_1:def_7
.= (((b |^ (m2 + 1)) * (a |^ (l1 + 1))) * (n choose (m2 + 1))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2))) by Th20
.= ((b |^ (m2 + 1)) * ((n choose (m2 + 1)) * (a |^ (l1 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2))) by Th20
.= ((b |^ (m2 + 1)) * ((a |^ (l1 + 1)) * (n choose (m2 + 1)))) + ((b |^ (m2 + 1)) * ((n choose m2) * (a |^ l2))) by Th17
.= (((a |^ (l1 + 1)) * (n choose (m2 + 1))) + ((n choose m2) * (a |^ l2))) * (b |^ (m2 + 1)) by VECTSP_1:def_7
.= (((n choose (m2 + 1)) * (a |^ (l1 + 1))) + ((n choose m2) * (a |^ (l1 + 1)))) * (b |^ (m2 + 1)) by Th17
.= (((n choose (m2 + 1)) + (n choose m2)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1)) by Th15
.= (((n + 1) choose (m2 + 1)) * (a |^ (l1 + 1))) * (b |^ (m2 + 1)) by NEWTON:22
.= ((a,b) In_Power (n + 1)) /. i by A13, A41, Def7
.= ((a,b) In_Power (n + 1)) . i by A13, PARTFUN1:def_6 ; ::_thesis: verum
end;
A44: ( i in {1} implies (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i )
proof
assume i in {1} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then A45: i = 1 by TARSKI:def_1;
then A46: F2 /. i = (<*(0. R)*> ^ (((a,b) In_Power n) * b)) . 1 by A17, PARTFUN1:def_6
.= 0. R by FINSEQ_1:41 ;
n + 1 >= 0 + 1 by XREAL_1:6;
then 1 in Seg (n + 1) by FINSEQ_1:1;
then A47: 1 in Seg (len ((a,b) In_Power n)) by Def7;
then A48: 1 in dom ((a,b) In_Power n) by FINSEQ_1:def_3;
then A49: ((a,b) In_Power n) /. i = ((a,b) In_Power n) . i by A45, PARTFUN1:def_6;
A50: 1 in dom (((a,b) In_Power n) * a) by A2, A47, FINSEQ_1:def_3;
A51: F1 /. i = ((((a,b) In_Power n) * a) ^ <*(0. R)*>) . 1 by A16, A45, PARTFUN1:def_6
.= (((a,b) In_Power n) * a) . 1 by A50, FINSEQ_1:def_7
.= (((a,b) In_Power n) * a) /. 1 by A50, PARTFUN1:def_6
.= (((a,b) In_Power n) /. 1) * a by A48, POLYNOM1:def_2
.= (a |^ n) * a by A45, A49, Th23
.= a |^ (n + 1) by GROUP_1:def_7 ;
thus (F1 + F2) . i = (F1 + F2) /. i by A29, PARTFUN1:def_6
.= (F1 /. i) + (F2 /. i) by A9, A18, Def1
.= a |^ (n + 1) by A51, A46, RLVECT_1:def_4
.= ((a,b) In_Power (n + 1)) . i by A45, Th23 ; ::_thesis: verum
end;
now__::_thesis:_(_i_in_({1}_\/__{__k_where_k_is_Element_of_NAT_:_(_1_<_k_&_k_<_(n_+_1)_+_1_)__}__)_\/_{((n_+_1)_+_1)}_implies_(F1_+_F2)_._i_=_((a,b)_In_Power_(n_+_1))_._i_)
assume i in ({1} \/ { k where k is Element of NAT : ( 1 < k & k < (n + 1) + 1 ) } ) \/ {((n + 1) + 1)} ; ::_thesis: (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i
then ( i in {1} \/ { k where k is Element of NAT : ( 1 < k & k < (n + 1) + 1 ) } or i in {((n + 1) + 1)} ) by XBOOLE_0:def_3;
hence (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i by A44, A19, A30, XBOOLE_0:def_3; ::_thesis: verum
end;
hence (F1 + F2) . i = ((a,b) In_Power (n + 1)) . i by A12, A13, NAT_1:12, NEWTON:1; ::_thesis: verum
end;
assume S1[n] ; ::_thesis: S1[n + 1]
then A52: (a + b) |^ (n + 1) = (Sum ((a,b) In_Power n)) * (a + b) by GROUP_1:def_7
.= ((Sum ((a,b) In_Power n)) * a) + ((Sum ((a,b) In_Power n)) * b) by VECTSP_1:def_2
.= (Sum (((a,b) In_Power n) * a)) + ((Sum ((a,b) In_Power n)) * b) by Th5
.= (Sum (((a,b) In_Power n) * a)) + (Sum (((a,b) In_Power n) * b)) by Th5 ;
A53: Sum F1 = (Sum (((a,b) In_Power n) * a)) + (Sum <*(0. R)*>) by RLVECT_1:41
.= (Sum (((a,b) In_Power n) * a)) + (0. R) by Th3
.= Sum (((a,b) In_Power n) * a) by RLVECT_1:def_4 ;
A54: Sum F2 = (Sum <*(0. R)*>) + (Sum (((a,b) In_Power n) * b)) by RLVECT_1:41
.= (0. R) + (Sum (((a,b) In_Power n) * b)) by Th3
.= Sum (((a,b) In_Power n) * b) by ALGSTR_1:def_2 ;
dom F1 = Seg (len F1) by FINSEQ_1:def_3
.= dom F2 by A4, A5, FINSEQ_1:def_3 ;
then A55: Sum (((((a,b) In_Power n) * a) ^ <*(0. R)*>) + (<*(0. R)*> ^ (((a,b) In_Power n) * b))) = (Sum (((a,b) In_Power n) * a)) + (Sum (((a,b) In_Power n) * b)) by A53, A54, Th7;
len ((a,b) In_Power (n + 1)) = len (F1 + F2) by A7, Def7;
hence S1[n + 1] by A52, A55, A8, FINSEQ_1:14; ::_thesis: verum
end;
(a + b) |^ 0 = 1_ R by Th8
.= Sum <*(1_ R)*> by Th3
.= Sum ((a,b) In_Power 0) by Th22 ;
then A56: S1[ 0 ] ;
for n being Element of NAT holds S1[n] from NAT_1:sch_1(A56, A1);
hence (a + b) |^ n = Sum ((a,b) In_Power n) ; ::_thesis: verum
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;