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