:: The Binomial Theorem for Algebraic Structures :: by Christoph Schwarzweller :: :: Received November 20, 2000 :: Copyright (c) 2000 Association of Mizar Users environ vocabularies RLVECT_1, ALGSTR_1, VECTSP_2, ARYTM_1, BINOP_1, LATTICES, GROUP_1, VECTSP_1, ALGSTR_2, FUNCT_1, FUNCT_2, MCART_1, RELAT_1, FINSEQ_1, FINSEQ_4, NEWTON, FINSEQ_2, BOOLE, BINOM, ARYTM, ALGSTR_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, XCMPLX_0, STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_1, FUNCT_2, NAT_1, FINSEQ_1, RELSET_1, BINOP_1, ALGSTR_1, FINSEQ_2, VECTSP_1, VECTSP_2, GROUP_1, NEWTON, RLVECT_1, MCART_1, POLYNOM1, XXREAL_0; constructors BINOP_1, XXREAL_0, REAL_1, NAT_1, NEWTON, ALGSTR_1, MONOID_0, POLYNOM1; registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, INT_1, ALGSTR_0; requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM; definitions BINOP_1, ALGSTR_0; theorems TARSKI, FUNCT_2, VECTSP_1, RLVECT_1, ALGSTR_1, NAT_1, MCART_1, FINSEQ_1, GROUP_1, NEWTON, FINSEQ_2, FUNCT_1, ZFMISC_1, INT_1, RELSET_1, RELAT_1, POLYNOM1, XBOOLE_0, XREAL_1, PARTFUN1, ORDINAL1, ALGSTR_0; schemes NAT_1, RECDEF_1, POLYNOM2; begin :: Preliminaries :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: registration cluster Abelian right_add-cancelable -> left_add-cancelable (non empty addLoopStr); coherence proof let R be non empty addLoopStr; assume R is Abelian right_add-cancelable; then reconsider R as Abelian right_add-cancelable (non empty addLoopStr); R is left_add-cancelable proof let a,b,c be Element of R; assume a + b = a + c; hence b = c by ALGSTR_0:def 4; end; hence thesis; end; cluster Abelian left_add-cancelable -> right_add-cancelable (non empty addLoopStr); coherence proof let R be non empty addLoopStr; assume R is Abelian left_add-cancelable; then reconsider R as Abelian left_add-cancelable (non empty addLoopStr); R is right_add-cancelable proof let a,b,c be Element of R; assume b + a = c + a; hence b = c by ALGSTR_0:def 3; end; hence thesis; end; end; registration cluster right_zeroed right_complementable add-associative -> right_add-cancelable (non empty addLoopStr); coherence; end; registration cluster Abelian add-associative left_zeroed right_zeroed commutative associative add-cancelable distributive unital (non empty doubleLoopStr); existence proof consider R being comRing; take R; thus thesis; end; end; theorem Th1: for R being right_zeroed left_add-cancelable left-distributive (non empty doubleLoopStr), a being Element of R holds 0.R * a = 0.R proof let R be right_zeroed left_add-cancelable left-distributive (non empty doubleLoopStr), a be Element of R; 0.R * a = (0.R + 0.R) * a by RLVECT_1:def 7 .= 0.R * a + 0.R * a by VECTSP_1:def 12; then 0.R * a + 0.R * a = 0.R * a + 0.R by RLVECT_1:def 7; hence 0.R * a = 0.R by ALGSTR_0:def 3; end; theorem Th2: for R being left_zeroed right_add-cancelable right-distributive (non empty doubleLoopStr), a being Element of R holds a * 0.R = 0.R proof let R be left_zeroed right_add-cancelable right-distributive (non empty doubleLoopStr), a be Element of R; a * 0.R = a * (0.R + 0.R) by ALGSTR_1:def 5 .= a * 0.R + a * 0.R by VECTSP_1:def 11; then a * 0.R + a * 0.R = 0.R + a * 0.R by ALGSTR_1:def 5; hence thesis by ALGSTR_0:def 4; end; scheme RecDef1 {C,D() -> non empty set, b() -> Element of D(), F() -> 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)) proof A1: for a being Element of C() holds 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(); defpred P[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 P[n,x,y]; ex f being Function of NAT,D() st f.0 = b() & for n being Element of NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2 (A2); hence thesis; end; ex g being Function of C(),Funcs(NAT,D()) st for a being Element of C() holds ex f being Function of NAT,D() st g.a = f & f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(a,f.n) proof set h = {[a,l] where a is Element of C(), l is Element of Funcs(NAT,D()) : ex f being Function of NAT,D() st f = l & f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(a,f.n) }; A3: now let x,y1,y2 be set; assume A4: [x,y1] in h & [x,y2] in h; then consider a1 being Element of C(), l1 being Element of Funcs(NAT,D()) such that A5: [x,y1] = [a1,l1] & 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); consider f1 being Function of NAT,D() such that A6: f1 = l1 & f1.0 = b() & for n being Element of NAT holds f1.(n+1) = F().(a1,f1.n) by A5; consider a2 being Element of C(), l2 being Element of Funcs(NAT,D()) such that A7: [x,y2] = [a2,l2] & 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 A4; consider f2 being Function of NAT,D() such that A8: f2 = l2 & f2.0 = b() & for n being Element of NAT holds f2.(n+1) = F().(a2,f2.n) by A7; A9: a1 = [x,y1]`1 by A5,MCART_1:def 1 .= x by MCART_1:def 1 .= [a2,l2]`1 by A7,MCART_1:def 1 .= a2 by MCART_1:def 1; A10: NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1; A11: now let x be set; assume x in NAT; then reconsider x' = x as Element of NAT; defpred P[Element of NAT] means f1.$1 = f2.$1; A12: P[0] by A6,A8; A13: now let n be Element of NAT; assume A14: P[n]; f1.(n+1) = F().(a2,f1.n) by A6,A9 .= f2.(n+1) by A8,A14; hence P[n+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A12,A13); hence f1.x = f2.x' .= f2.x; end; thus y1 = [a1,l1]`2 by A5,MCART_1:def 2 .= l1 by MCART_1:def 2 .= l2 by A6,A8,A10,A11,FUNCT_1:9 .= [x,y2]`2 by A7,MCART_1:def 2 .= y2 by MCART_1:def 2; end; now let x be set; assume x in h; then consider a being Element of C(), l being Element of Funcs(NAT,D()) such that A15: 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); thus x in [:C(),Funcs(NAT,D()):] by A15,ZFMISC_1:def 2; end; then h c= [:C(),Funcs(NAT,D()):] by TARSKI:def 3; then reconsider h as Relation of C(),Funcs(NAT,D()) by RELSET_1:def 1; A16: for x being set holds x in dom h implies x in C(); for x being set holds x in C() implies x in dom h proof let x be set; assume A17: x in C(); then consider f being Function of NAT,D() such that A18: f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(x,f.n) by A1; reconsider f' = f as Element of Funcs(NAT,D()) by FUNCT_2:11; [x,f'] in h by A17,A18; hence thesis by RELAT_1:def 4; end; then dom h = C() by A16,TARSKI:2; then reconsider h as Function of C(),Funcs(NAT,D()) by A3,FUNCT_1:def 1,FUNCT_2:def 1; take h; for a being Element of C() holds 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(); dom h = C() by FUNCT_2:def 1; then [a,h.a] in h by FUNCT_1:8; then consider a' being Element of C(), l being Element of Funcs(NAT,D()) such that A19: [a,h.a] = [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); consider f' being Function of NAT,D() such that A20: f' = l & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(a',f'.n) by A19; A21: a = [a',l]`1 by A19,MCART_1:def 1 .= a' by MCART_1:def 1; h.a = [a',l]`2 by A19,MCART_1:def 2 .= l by MCART_1:def 2; hence thesis by A20,A21; end; hence thesis; end; then consider g being Function of C(),Funcs(NAT,D()) such that A22: for a being Element of C() holds 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 }; A23: now let x,y1,y2 be set; assume A24: [x,y1] in h & [x,y2] in h; then consider n1 being Element of NAT, a1 being Element of C(), z1 being Element of D() such that A25: [x,y1] = [[n1,a1],z1] & ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1; consider n2 being Element of NAT, a2 being Element of C(), z2 being Element of D() such that A26: [x,y2] = [[n2,a2],z2] & ex f2 being Function of NAT,D() st f2 = g.a2 & z2 = f2.n2 by A24; A27: [n1,a1] = [x,y1]`1 by A25,MCART_1:def 1 .= x by MCART_1:def 1 .= [[n2,a2],z2]`1 by A26,MCART_1:def 1 .= [n2,a2] by MCART_1:def 1; then A28: n1 = [n2,a2]`1 by MCART_1:def 1 .= n2 by MCART_1:def 1; a1 = [n2,a2]`2 by A27,MCART_1:def 2 .= a2 by MCART_1:def 2; hence y1 = [x,y2]`2 by A25,A26,A28,MCART_1:def 2 .= y2 by MCART_1:def 2; end; now let x be set; assume x in h; then consider n1 being Element of NAT, a1 being Element of C(), z1 being Element of D() such that A29: x = [[n1,a1],z1] & 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 A29,ZFMISC_1:def 2; end; then h c= [:[:NAT,C():],D():] by TARSKI:def 3; then reconsider h as Relation of [:NAT,C():],D() by RELSET_1:def 1; A30: for x being set holds x in dom h implies x in [:NAT,C():]; for x being set holds x in [:NAT,C():] implies x in dom h proof let x be set; assume x in [:NAT,C():]; then consider n,d being set such that A31: n in NAT & d in C() & x = [n,d] by ZFMISC_1:def 2; reconsider n as Element of NAT by A31; reconsider d as Element of C() by A31; consider f' being Function of NAT,D() such that A32: g.d = f' & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(d,f'.n) by A22; ex z being Element of D() st ex f being Function of NAT,D() st f = g.d & z = f.n proof take f'.n; take f'; thus thesis by A32; end; then consider z being Element of D() such that A33: ex f being Function of NAT,D() st f = g.d & z = f.n; [x,z] in h by A31,A33; hence thesis by RELAT_1:def 4; end; then dom h = [:NAT,C():] by A30,TARSKI:2; then reconsider h as Function of [:NAT,C():],D() by A23,FUNCT_1:def 1,FUNCT_2:def 1; take h; 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(); consider f' being Function of NAT,D() such that A34: g.a = f' & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(a,f'.n) by A22; [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 A35: [[0,a],u] in h by RELAT_1:def 4; consider n being Element of NAT, d being Element of C(), z being Element of D() such that A36: [[0,a],u] = [[n,d],z] & ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A35; consider f1 being Function of NAT,D() such that A37: f1 = g.d & z = f1.n by A36; A38: [0,a] = [[n,d],z]`1 by A36,MCART_1:def 1 .= [n,d] by MCART_1:def 1; then A39: n = [0,a]`1 by MCART_1:def 1 .= 0 by MCART_1:def 1; A40: u = [[n,d],z]`2 by A36,MCART_1:def 2 .= z by MCART_1:def 2; A41: d = [0,a]`2 by A38,MCART_1:def 2 .= a by MCART_1:def 2; now let k be Element of NAT; [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 A42: [[k+1,a],u] in h by RELAT_1:def 4; consider n being Element of NAT, d being Element of C(), z being Element of D() such that A43: [[k+1,a],u] = [[n,d],z] & ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A42; consider f1 being Function of NAT,D() such that A44: f1 = g.d & z = f1.n by A43; A45: [k+1,a] = [[n,d],z]`1 by A43,MCART_1:def 1 .= [n,d] by MCART_1:def 1; then A46: n = [k+1,a]`1 by MCART_1:def 1 .= k+1 by MCART_1:def 1; A47: u = [[n,d],z]`2 by A43,MCART_1:def 2 .= z by MCART_1:def 2; A48: d = [k+1,a]`2 by A45,MCART_1:def 2 .= a by MCART_1:def 2; [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 A49: [[k,a],v] in h by RELAT_1:def 4; consider n1 being Element of NAT, d1 being Element of C(), z1 being Element of D() such that A50: [[k,a],v] = [[n1,d1],z1] & ex f2 being Function of NAT,D() st f2 = g.d1 & z1 = f2.n1 by A49; consider f2 being Function of NAT,D() such that A51: f2 = g.d1 & z1 = f2.n1 by A50; A52: [k,a] = [[n1,d1],z1]`1 by A50,MCART_1:def 1 .= [n1,d1] by MCART_1:def 1; then A53: n1 = [k,a]`1 by MCART_1:def 1 .= k by MCART_1:def 1; A54: v = [[n1,d1],z1]`2 by A50,MCART_1:def 2 .= z1 by MCART_1:def 2; A55: d1 = [k,a]`2 by A52,MCART_1:def 2 .= a by MCART_1:def 2; thus h.(k+1,a) = f'.(k+1) by A34,A42,A44,A46,A47,A48,FUNCT_1:8 .= F().(a,z1) by A34,A51,A53,A55 .= F().(a,h.(k,a)) by A49,A54,FUNCT_1:8; end; hence thesis by A34,A35,A37,A39,A40,A41,FUNCT_1:8; end; hence thesis; end; scheme RecDef2 {C,D() -> non empty set, b() -> Element of D(), F() -> 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) proof A1: for a being Element of C() holds 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(); defpred P[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 P[n,x,y]; ex f being Function of NAT,D() st f.0 = b() & for n being Element of NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2 (A2); hence thesis; end; ex g being Function of C(),Funcs(NAT,D()) st for a being Element of C() holds ex f being Function of NAT,D() st g.a = f & f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(f.n,a) proof set h = {[a,l] where a is Element of C(), l is Element of Funcs(NAT,D()) : ex f being Function of NAT,D() st f = l & f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(f.n,a) }; A3: now let x,y1,y2 be set; assume A4: [x,y1] in h & [x,y2] in h; then consider a1 being Element of C(), l1 being Element of Funcs(NAT,D()) such that A5: [x,y1] = [a1,l1] & 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); consider f1 being Function of NAT,D() such that A6: f1 = l1 & f1.0 = b() & for n being Element of NAT holds f1.(n+1) = F().(f1.n,a1) by A5; consider a2 being Element of C(), l2 being Element of Funcs(NAT,D()) such that A7: [x,y2] = [a2,l2] & 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 A4; consider f2 being Function of NAT,D() such that A8: f2 = l2 & f2.0 = b() & for n being Element of NAT holds f2.(n+1) = F().(f2.n,a2) by A7; A9: a1 = [x,y1]`1 by A5,MCART_1:def 1 .= x by MCART_1:def 1 .= [a2,l2]`1 by A7,MCART_1:def 1 .= a2 by MCART_1:def 1; A10: NAT = dom f1 & NAT = dom f2 by FUNCT_2:def 1; A11: now let x be set; assume x in NAT; then reconsider x' = x as Element of NAT; defpred P[Element of NAT] means f1.$1 = f2.$1; A12: P[0] by A6,A8; A13: now let n be Element of NAT; assume A14: P[n]; f1.(n+1) = F().(f1.n,a2) by A6,A9 .= f2.(n+1) by A8,A14; hence P[n+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A12,A13); hence f1.x = f2.x' .= f2.x; end; thus y1 = [a1,l1]`2 by A5,MCART_1:def 2 .= l1 by MCART_1:def 2 .= l2 by A6,A8,A10,A11,FUNCT_1:9 .= [x,y2]`2 by A7,MCART_1:def 2 .= y2 by MCART_1:def 2; end; now let x be set; assume x in h; then consider a being Element of C(), l being Element of Funcs(NAT,D()) such that A15: 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); thus x in [:C(),Funcs(NAT,D()):] by A15,ZFMISC_1:def 2; end; then h c= [:C(),Funcs(NAT,D()):] by TARSKI:def 3; then reconsider h as Relation of C(),Funcs(NAT,D()) by RELSET_1:def 1; A16: for x being set holds x in dom h implies x in C(); for x being set holds x in C() implies x in dom h proof let x be set; assume A17: x in C(); then consider f being Function of NAT,D() such that A18: f.0 = b() & for n being Element of NAT holds f.(n+1) = F().(f.n,x) by A1; reconsider f' = f as Element of Funcs(NAT,D()) by FUNCT_2:11; [x,f'] in h by A17,A18; hence thesis by RELAT_1:def 4; end; then dom h = C() by A16,TARSKI:2; then reconsider h as Function of C(),Funcs(NAT,D()) by A3,FUNCT_1:def 1,FUNCT_2:def 1; take h; for a being Element of C() holds 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(); dom h = C() by FUNCT_2:def 1; then [a,h.a] in h by FUNCT_1:8; then consider a' being Element of C(), l being Element of Funcs(NAT,D()) such that A19: [a,h.a] = [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'); consider f' being Function of NAT,D() such that A20: f' = l & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(f'.n,a') by A19; A21: a = [a',l]`1 by A19,MCART_1:def 1 .= a' by MCART_1:def 1; h.a = [a',l]`2 by A19,MCART_1:def 2 .= l by MCART_1:def 2; hence thesis by A20,A21; end; hence thesis; end; then consider g being Function of C(),Funcs(NAT,D()) such that A22: for a being Element of C() holds 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 }; A23: now let x,y1,y2 be set; assume A24: [x,y1] in h & [x,y2] in h; then consider n1 being Element of NAT, a1 being Element of C(), z1 being Element of D() such that A25: [x,y1] = [[a1,n1],z1] & ex f1 being Function of NAT,D() st f1 = g.a1 & z1 = f1.n1; consider n2 being Element of NAT, a2 being Element of C(), z2 being Element of D() such that A26: [x,y2] = [[a2,n2],z2] & ex f2 being Function of NAT,D() st f2 = g.a2 & z2 = f2.n2 by A24; A27: [a1,n1] = [x,y1]`1 by A25,MCART_1:def 1 .= x by MCART_1:def 1 .= [[a2,n2],z2]`1 by A26,MCART_1:def 1 .= [a2,n2] by MCART_1:def 1; then A28: a1 = [a2,n2]`1 by MCART_1:def 1 .= a2 by MCART_1:def 1; n1 = [a2,n2]`2 by A27,MCART_1:def 2 .= n2 by MCART_1:def 2; hence y1 = [x,y2]`2 by A25,A26,A28,MCART_1:def 2 .= y2 by MCART_1:def 2; end; now let x be set; assume x in h; then consider n1 being Element of NAT, a1 being Element of C(), z1 being Element of D() such that A29: x = [[a1,n1],z1] & 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 A29,ZFMISC_1:def 2; end; then h c= [:[:C(),NAT:],D():] by TARSKI:def 3; then reconsider h as Relation of [:C(),NAT:],D() by RELSET_1:def 1; A30: for x being set holds x in dom h implies x in [:C(),NAT:]; for x being set holds x in [:C(),NAT:] implies x in dom h proof let x be set; assume x in [:C(),NAT:]; then consider d,n being set such that A31: d in C() & n in NAT & x = [d,n] by ZFMISC_1:def 2; reconsider n as Element of NAT by A31; reconsider d as Element of C() by A31; consider f' being Function of NAT,D() such that A32: g.d = f' & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(f'.n,d) by A22; ex z being Element of D() st ex f being Function of NAT,D() st f = g.d & z = f.n proof take f'.n; take f'; thus thesis by A32; end; then consider z being Element of D() such that A33: ex f being Function of NAT,D() st f = g.d & z = f.n; [x,z] in h by A31,A33; hence thesis by RELAT_1:def 4; end; then dom h = [:C(),NAT:] by A30,TARSKI:2; then reconsider h as Function of [:C(),NAT:],D() by A23,FUNCT_1:def 1,FUNCT_2:def 1; take h; 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(); consider f' being Function of NAT,D() such that A34: g.a = f' & f'.0 = b() & for n being Element of NAT holds f'.(n+1) = F().(f'.n,a) by A22; [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 A35: [[a,0],u] in h by RELAT_1:def 4; consider n being Element of NAT, d being Element of C(), z being Element of D() such that A36: [[a,0],u] = [[d,n],z] & ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A35; consider f1 being Function of NAT,D() such that A37: f1 = g.d & z = f1.n by A36; A38: [a,0] = [[d,n],z]`1 by A36,MCART_1:def 1 .= [d,n] by MCART_1:def 1; then A39: n = [a,0]`2 by MCART_1:def 2 .= 0 by MCART_1:def 2; A40: u = [[d,n],z]`2 by A36,MCART_1:def 2 .= z by MCART_1:def 2; A41: d = [a,0]`1 by A38,MCART_1:def 1 .= a by MCART_1:def 1; now let k be Element of NAT; [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 A42: [[a,k+1],u] in h by RELAT_1:def 4; consider n being Element of NAT, d being Element of C(), z being Element of D() such that A43: [[a,k+1],u] = [[d,n],z] & ex f1 being Function of NAT,D() st f1 = g.d & z = f1.n by A42; consider f1 being Function of NAT,D() such that A44: f1 = g.d & z = f1.n by A43; A45: [a,k+1] = [[d,n],z]`1 by A43,MCART_1:def 1 .= [d,n] by MCART_1:def 1; then A46: n = [a,k+1]`2 by MCART_1:def 2 .= k+1 by MCART_1:def 2; A47: u = [[d,n],z]`2 by A43,MCART_1:def 2 .= z by MCART_1:def 2; A48: d = [a,k+1]`1 by A45,MCART_1:def 1 .= a by MCART_1:def 1; [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 A49: [[a,k],v] in h by RELAT_1:def 4; consider n1 being Element of NAT, d1 being Element of C(), z1 being Element of D() such that A50: [[a,k],v] = [[d1,n1],z1] & ex f2 being Function of NAT,D() st f2 = g.d1 & z1 = f2.n1 by A49; consider f2 being Function of NAT,D() such that A51: f2 = g.d1 & z1 = f2.n1 by A50; A52: [a,k] = [[d1,n1],z1]`1 by A50,MCART_1:def 1 .= [d1,n1] by MCART_1:def 1; then A53: n1 = [a,k]`2 by MCART_1:def 2 .= k by MCART_1:def 2; A54: v = [[d1,n1],z1]`2 by A50,MCART_1:def 2 .= z1 by MCART_1:def 2; A55: d1 = [a,k]`1 by A52,MCART_1:def 1 .= a by MCART_1:def 1; thus h.(a,k+1) = f'.n by A34,A42,A44,A47,A48,FUNCT_1:8 .= F().(f2.n1,a) by A34,A46,A51,A53,A55 .= F().(h.(a,k),a) by A49,A51,A54,FUNCT_1:8; end; hence thesis by A34,A35,A37,A39,A40,A41,FUNCT_1:8; end; hence thesis; end; begin :: On Finite Sequences :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: theorem Th3: for L being left_zeroed (non empty addLoopStr), a being Element of L holds Sum <* a *> = a proof let V be left_zeroed (non empty addLoopStr), v be Element of 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(S) = f.(len S) and A2: f.0 = 0.V and A3: for j being Element of NAT for v being Element of V st j < len S & v = S.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 13; A4: len <* a *> = 1 by FINSEQ_1:56; 0 < 1; then consider j being Element of NAT such that A5: j < len S by A4; A6: j = 0 by A4,A5,NAT_1:14; S.(j + 1) = S.(0 + 1) by A4,A5,NAT_1:14 .= v by FINSEQ_1:57; then f.1 = 0.V + v by A2,A3,A5,A6 .= a by ALGSTR_1:def 5; hence thesis by A1,FINSEQ_1:56; end; theorem for R being left_zeroed right_add-cancelable right-distributive (non empty doubleLoopStr), a being Element of R, p being FinSequence of the carrier of R holds Sum(a * p) = a * Sum p proof let R be left_zeroed right_add-cancelable right-distributive (non empty doubleLoopStr), a be Element of R, p be FinSequence of the carrier of R; consider f being Function of NAT,the carrier of R such that A1: Sum p = f.(len p) & f.0 = 0.R & for j being Element of NAT, v being Element of R st j < len p & v = p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 13; consider fa being Function of NAT,the carrier of R such that A2: Sum(a * p) = fa.(len(a * p)) & fa.0 = 0.R & for j being Element of NAT, 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 13; A3: Seg(len(a * p)) = dom(a * p) by FINSEQ_1:def 3 .= dom p by POLYNOM1:def 2 .= Seg(len p) by FINSEQ_1:def 3; defpred P[Element of NAT] means a * f.$1 = fa.$1; A4: P[0] by A1,A2,Th2; A5: now let j be Element of NAT; assume A6: 0 <= j & j < len p; thus P[j] implies P[j+1] proof assume A7: P[j]; A8: j < len(a * p) by A3,A6,FINSEQ_1:8; then A9: j + 1 <= len(a * p) by NAT_1:13; A10: j + 1 <= len p by A6,NAT_1:13; A11: 0 + 1 <= j + 1 by XREAL_1:8; then j + 1 in Seg len(a * p) by A9,FINSEQ_1:3; 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 8; j + 1 in Seg len p by A10,A11,FINSEQ_1:3; then A13: j + 1 in dom p by FINSEQ_1:def 3; then A14: p/.(j + 1) = p.(j + 1) by PARTFUN1:def 8; thus fa.(j+1) = a * f.j + (a * p)/.(j + 1) by A2,A7,A8,A12 .= a * f.j + a * p/.(j + 1) by A13,POLYNOM1:def 2 .= a * (f.j + p/.(j + 1)) by VECTSP_1:def 11 .= a * f.(j+1) by A1,A6,A14; end; end; A15: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from POLYNOM2:sch 4 (A4,A5); thus Sum(a * p) = fa.(len p) by A2,A3,FINSEQ_1:8 .= a * Sum p by A1,A15; end; theorem Th5: for R being right_zeroed left_add-cancelable left-distributive (non empty doubleLoopStr), a being Element of R, p being FinSequence of the carrier of R holds Sum(p * a) = Sum p * a proof let R be right_zeroed left_add-cancelable left-distributive (non empty doubleLoopStr), a be Element of R, p be FinSequence of the carrier of R; consider f being Function of NAT,the carrier of R such that A1: Sum p = f.(len p) & f.0 = 0.R & for j being Element of NAT, v being Element of R st j < len p & v = p.(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 13; consider fa being Function of NAT,the carrier of R such that A2: Sum(p * a) = fa.(len(p * a)) & fa.0 = 0.R & for j being Element of NAT, 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 13; A3: Seg(len(p * a)) = dom(p * a) by FINSEQ_1:def 3 .= dom p by POLYNOM1:def 3 .= Seg(len p) by FINSEQ_1:def 3; defpred P[Element of NAT] means f.$1 * a = fa.$1; A4: P[0] by A1,A2,Th1; A5: now let j be Element of NAT; assume A6: 0 <= j & j < len p; thus P[j] implies P[j+1] proof assume A7: f.j * a = fa.j; A8: j < len(p * a) by A3,A6,FINSEQ_1:8; then A9: j + 1 <= len(p * a) by NAT_1:13; A10: 0 + 1 <= j + 1 by XREAL_1:8; then j + 1 in Seg len(p * a) by A9,FINSEQ_1:3; then j + 1 in dom(p * a) by FINSEQ_1:def 3; then A11: (p * a)/.(j + 1) = (p * a).(j + 1) by PARTFUN1:def 8; j + 1 in Seg len p by A3,A9,A10,FINSEQ_1:3; then A12: j + 1 in dom p by FINSEQ_1:def 3; then A13: p/.(j + 1) = p.(j + 1) by PARTFUN1:def 8; thus fa.(j+1) = f.j * a + (p * a)/.(j + 1) by A2,A7,A8,A11 .= f.j * a + p/.(j + 1) * a by A12,POLYNOM1:def 3 .= (f.j + p/.(j + 1)) * a by VECTSP_1:def 12 .= f.(j+1) * a by A1,A6,A13; end; end; A14: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from POLYNOM2:sch 4 (A4,A5); thus Sum(p * a) = fa.(len p) by A2,A3,FINSEQ_1:8 .= Sum p * a by A1,A14; end; theorem for R being commutative (non empty doubleLoopStr), a being Element of R, p being FinSequence of the carrier of R holds Sum(p * a) = Sum(a * p) proof let R be commutative (non empty doubleLoopStr), a be Element of R, p be FinSequence of the carrier of R; consider f being Function of NAT,the carrier of R such that A1: Sum(p * a) = f.(len(p * a)) & f.0 = 0.R & for j being Element of NAT, v being Element of R st j < len(p * a) & v = (p * a).(j + 1) holds f.(j + 1) = f.j + v by RLVECT_1:def 13; consider g being Function of NAT,the carrier of R such that A2: Sum(a * p) = g.(len(a * p)) & g.0 = 0.R & for j being Element of NAT, v being Element of R st j < len(a * p) & v = (a * p).(j + 1) holds g.(j + 1) = g.j + v by RLVECT_1:def 13; A3: Seg(len(a * p)) = dom(a * p) by FINSEQ_1:def 3 .= dom p by POLYNOM1:def 2 .= Seg(len p) by FINSEQ_1:def 3; A4: Seg(len(p * a)) = dom(p * a) by FINSEQ_1:def 3 .= dom p by POLYNOM1:def 3 .= Seg(len p) by FINSEQ_1:def 3; defpred P[Element of NAT] means f.$1 = g.$1; A5: P[0] by A1,A2; A6: now let j be Element of NAT; assume A7: 0 <= j & j < len p; thus P[j] implies P[j+1] proof assume A8: f.j = g.j; A9: j < len(p * a) by A4,A7,FINSEQ_1:8; then A10: j + 1 <= len(p * a) by NAT_1:13; A11: 0 + 1 <= j + 1 by XREAL_1:8; then j + 1 in Seg len(p * a) by A10,FINSEQ_1:3; then j + 1 in dom(p * a) by FINSEQ_1:def 3; then A12: (p * a)/.(j + 1) = (p * a).(j + 1) by PARTFUN1:def 8; A13: j < len(a * p) by A3,A7,FINSEQ_1:8; j + 1 in Seg len(a * p) by A3,A4,A10,A11,FINSEQ_1:3; then A14: j + 1 in dom(a * p) by FINSEQ_1:def 3; then A15: j + 1 in dom p by POLYNOM1:def 2; A16: (a * p)/.(j + 1) = (a * p).(j + 1) by A14,PARTFUN1:def 8; thus f.(j+1) = g.j + (p * a)/.(j + 1) by A1,A8,A9,A12 .= g.j + p/.(j + 1) * a by A15,POLYNOM1:def 3 .= g.j + (a * p)/.(j + 1) by A15,POLYNOM1:def 2 .= g.(j+1) by A2,A13,A16; end; end; A17: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from POLYNOM2:sch 4 (A5,A6); thus Sum(p * a) = f.(len p) by A1,A4,FINSEQ_1:8 .= g.(len p) by A17 .= Sum(a * p) by A2,A3,FINSEQ_1:8; end; definition canceled 3; let R be non empty addLoopStr, p,q be FinSequence of the carrier of R such that dom p = dom q; func p + q -> FinSequence of the carrier of R means :Def4: dom it = dom p & for i being Nat st 1 <= i & i <= len it holds it/.i = p/.i + q/.i; existence proof defpred P[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) ex x being Element of R st P[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 P[k,f/.k] from POLYNOM2:sch 1(A1); take f; A3: len f = len p by A2,FINSEQ_1:def 3; now let m be Nat; assume 1 <= m & m <= len f; then m in Seg(len p) by A3,FINSEQ_1:3; hence f/.m = p/.m + q/.m by A2; end; hence thesis by A2,FINSEQ_1:def 3; end; uniqueness proof let y1,y2 be FinSequence of the carrier of R; assume that A4: dom y1 = dom p & for i being Nat st 1 <= i & i <= len y1 holds y1/.i = p/.i + q/.i and A5: dom y2 = dom p & for i being Nat st 1 <= i & i <= len y2 holds y2/.i = p/.i + q/.i; A6: Seg(len y1) = dom y2 by A4,A5,FINSEQ_1:def 3 .= Seg(len y2) by FINSEQ_1:def 3; then A7: len y1 = len y2 by FINSEQ_1:8; now let i be Nat; assume A8: 1 <= i & i <= len y1; then i in Seg (len y1) & i in Seg (len y2) by A6,FINSEQ_1:3; then A9: i in dom y1 & i in dom y2 by FINSEQ_1:def 3; hence y1.i = y1/.i by PARTFUN1:def 8 .= p/.i + q/.i by A4,A8 .= y2/.i by A5,A7,A8 .= y2.i by A9,PARTFUN1:def 8; end; hence thesis by A6,FINSEQ_1:18,FINSEQ_1:8; end; end; theorem Th7: for R being Abelian right_zeroed add-associative (non empty addLoopStr), 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 Abelian right_zeroed add-associative (non empty addLoopStr), p,q be FinSequence of the carrier of R; assume A1: dom p = dom q; then A2: Seg(len p) = dom q by FINSEQ_1:def 3 .= Seg(len q) by FINSEQ_1:def 3; then A3: len q = len p by FINSEQ_1:8; A4: Seg(len p) = dom p by FINSEQ_1:def 3 .= dom(p+q) by A1,Def4 .= Seg(len(p+q)) by FINSEQ_1:def 3; then A5: len(p+q) = len p by FINSEQ_1:8; consider fp being Function of NAT,the carrier of R such that A6: Sum p = fp.(len p) & fp.0 = 0.R & for j being Element of NAT, v being Element of R st j < len p & v = p.(j + 1) holds fp.(j + 1) = fp.j + v by RLVECT_1:def 13; consider fq being Function of NAT,the carrier of R such that A7: Sum q = fq.(len q) & fq.0 = 0.R & for j being Element of NAT, v being Element of R st j < len q & v = q.(j + 1) holds fq.(j + 1) = fq.j + v by RLVECT_1:def 13; consider fa being Function of NAT,the carrier of R such that A8: Sum(p+q) = fa.(len(p+q)) & fa.0 = 0.R & for j being Element of NAT, 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 13; defpred P[Element of NAT] means fp.$1 + fq.$1 = fa.$1; A9: P[0] by A6,A7,A8,RLVECT_1:def 7; A10: now let j be Element of NAT; assume A11: 0 <= j & j < len p; thus P[j] implies P[j+1] proof assume A12: P[j]; A13: j + 1 <= len(p+q) by A5,A11,NAT_1:13; A14: j + 1 <= len p by A11,NAT_1:13; A15: 0 + 1 <= j + 1 by XREAL_1:8; then j + 1 in Seg len(p+q) by A13,FINSEQ_1:3; then j + 1 in dom(p+q) by FINSEQ_1:def 3; then A16: (p+q)/.(j + 1) = (p+q).(j + 1) by PARTFUN1:def 8; j + 1 in Seg len p by A14,A15,FINSEQ_1:3; then j + 1 in dom p by FINSEQ_1:def 3; then A17: p/.(j + 1) = p.(j + 1) by PARTFUN1:def 8; j + 1 in Seg len q by A2,A14,A15,FINSEQ_1:3; then j + 1 in dom q by FINSEQ_1:def 3; then A18: q/.(j + 1) = q.(j + 1) by PARTFUN1:def 8; fa.(j+1) = fa.j + (p+q)/.(j + 1) by A5,A8,A11,A16 .= (fp.j + fq.j) + (p/.(j + 1) + q/.(j + 1)) by A1,A12,A13,A15,Def4 .= fp.j + (fq.j + (p/.(j + 1) + q/.(j + 1))) by RLVECT_1:def 6 .= fp.j + (p/.(j + 1) + (fq.j + q/.(j + 1))) by RLVECT_1:def 6 .= (fp.j + p/.(j + 1)) + (fq.j + q/.(j + 1)) by RLVECT_1:def 6 .= fp.(j+1) + (fq.j + q/.(j + 1)) by A6,A11,A17 .= fp.(j+1) + fq.(j+1) by A3,A7,A11,A18; hence thesis; end; end; A19: for i being Element of NAT st 0 <= i & i <= len p holds P[i] from POLYNOM2:sch 4 (A9,A10); thus Sum(p + q) = fa.(len p) by A4,A8,FINSEQ_1:8 .= Sum p + Sum q by A3,A6,A7,A19; end; begin :: On Powers in Rings :::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let R be unital (non empty multMagma), a be Element of R, n be Nat; func a|^n -> Element of R equals power(R).(a,n); coherence proof reconsider n as Element of NAT by ORDINAL1:def 13; power(R).(a,n) is Element of R; hence thesis; end; end; theorem Th8: for R being unital (non empty multMagma), a being Element of R holds a|^0 = 1_R & a|^1 = a proof let R be unital (non empty multMagma), a be Element of R; thus a|^0 = 1_R by GROUP_1:def 8; 0 + 1 = 1; then power(R).(a,1) = power(R).(a,0) * a by GROUP_1:def 8 .= 1_R * a by GROUP_1:def 8 .= a by GROUP_1:def 5; hence thesis; end; canceled; theorem for R being unital associative commutative (non empty multMagma), a,b being Element of R, n being Element of NAT holds (a * b)|^n = (a|^n) * (b|^n) proof let R be unital associative commutative (non empty multMagma), a,b be Element of R, n be Element of NAT; defpred P[Element of NAT] means power(R).(a * b,$1) = power(R).(a,$1) * power(R).(b,$1); power(R).(a * b,0) = 1_R by GROUP_1:def 8 .= 1_R * 1_R by GROUP_1:def 5 .= power(R).(a,0) * 1_R by GROUP_1:def 8 .= power(R).(a,0) * power(R).(b,0) by GROUP_1:def 8; then A1: P[0]; A2: now let m be Element of NAT; assume P[m]; then power(R).(a * b,m+1) = (power(R).(a,m) * power(R).(b,m)) * (a * b) by GROUP_1:def 8 .= ((power(R).(a,m) * power(R).(b,m)) * a) * b by GROUP_1:def 4 .= ((power(R).(a,m) * a) * power(R).(b,m)) * b by GROUP_1:def 4 .= (power(R).(a,m) * a) * (power(R).(b,m) * b) by GROUP_1:def 4 .= power(R).(a,m+1) * (power(R).(b,m) * b) by GROUP_1:def 8 .= power(R).(a,m+1) * power(R).(b,m+1) by GROUP_1:def 8; hence P[m+1]; end; for m being Element of NAT holds P[m] from NAT_1:sch 1(A1,A2); hence (a * b)|^n = (a|^n) * (b|^n); end; theorem Th11: for R being unital associative (non empty multMagma), a being Element of R, n,m being Element of NAT holds a|^(n+m) = (a|^n) * (a|^m) proof let R be unital associative (non empty multMagma), a be Element of R, n,m be Element of NAT; defpred P[Element of NAT] means power(R).(a,n+$1) = power(R).(a,n) * power(R).(a,$1); power(R).(a,n + 0) = power(R).(a,n) * 1_R by GROUP_1:def 5 .= power(R).(a,n) * power(R).(a,0) by GROUP_1:def 8; then A1: P[0]; A2: now let m be Element of NAT; assume A3: P[m]; power(R).(a,n+(m+1)) = power(R).(a,(n+m)+1) .= (power(R).(a,n) * power(R).(a,m)) * a by A3,GROUP_1:def 8 .= power(R).(a,n) * (power(R).(a,m) * a) by GROUP_1:def 4 .= power(R).(a,n) * power(R).(a,(m+1)) by GROUP_1:def 8; hence P[m+1]; end; for m being Element of NAT holds P[m] from NAT_1:sch 1(A1,A2); hence a|^(n+m) = (a|^n) * (a|^m); end; theorem for R being unital associative (non empty multMagma), a being Element of R, n,m being Element of NAT holds (a|^n)|^m = a|^(n * m) proof let R be unital associative (non empty multMagma), a be Element of R, n,m be Element of NAT; defpred P[Element of NAT] means power(R).(a|^n,$1) = power(R).(a,n * $1); power(R).(a|^n,0) = 1_R by GROUP_1:def 8 .= power(R).(a,n * 0) by GROUP_1:def 8; then A1: P[0]; A2: now let m be Element of NAT; assume P[m]; then power(R).(a|^n,m+1) = a|^(n * m) * (a|^n) by GROUP_1:def 8 .= a|^(n * m + n) by Th11 .= power(R).(a,n * (m + 1)); hence P[m+1]; end; for k being Element of NAT holds P[k] from NAT_1:sch 1(A1,A2); hence (a|^n)|^m = a|^(n * m); end; begin :: On Element of NATural Products in Rings ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let R be non empty addLoopStr; func Nat-mult-left(R) -> Function of [:NAT,the carrier of R:],the carrier of R means :Def6: 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 proof set D = the carrier of R; consider g being Function of [:NAT,D:],D such that A1: for a being Element of D 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)) from RecDef1; take g; thus thesis by A1; end; uniqueness proof let f,g be Function of [:NAT,the carrier of R:],the carrier of R; 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); 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); defpred P[Element of NAT] means for a being Element of R holds f.($1,a) = g.($1,a); A4: P[0] proof let a be Element of R; thus f.(0,a) = 0.R by A2 .= g.(0,a) by A3; end; A5: now let n be Element of NAT; assume A6: P[n]; now let a be Element of R; thus f.(n+1,a) = a + f.(n,a) by A2 .= a + g.(n,a) by A6 .= g.(n+1,a) by A3; end; hence P[n+1]; end; A7: for n being Element of NAT holds P[n] from NAT_1:sch 1(A4,A5); A8: dom f = [:NAT,the carrier of R:] by FUNCT_2:def 1; A9: dom g = [:NAT,the carrier of R:] by FUNCT_2:def 1; now let x be set; assume x in [:NAT,the carrier of R:]; then consider u,v being set such that A10: u in NAT & v in the carrier of R & x = [u,v] by ZFMISC_1:def 2; reconsider u as Element of NAT by A10; reconsider v as Element of R by A10; thus f.x = f.(u,v) by A10 .= g.(u,v) by A7 .= g.x by A10; end; hence thesis by A8,A9,FUNCT_1:9; end; func Nat-mult-right(R) -> Function of [:the carrier of R,NAT:],the carrier of R means :Def7: 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 proof consider g being Function of [:the carrier of R,NAT:],the carrier of R such that A11: 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) from RecDef2; take g; thus thesis by A11; end; uniqueness proof let f,g be Function of [:the carrier of R,NAT:],the carrier of R; assume A12: 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; assume A13: 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; defpred P[Element of NAT] means for a being Element of R holds f.(a,$1) = g.(a,$1); A14: P[0] proof let a be Element of R; thus f.(a,0) = 0.R by A12 .= g.(a,0) by A13; end; A15: now let n be Element of NAT; assume A16: P[n]; now let a be Element of R; thus f.(a,n+1) = f.(a,n) + a by A12 .= g.(a,n) + a by A16 .= g.(a,n+1) by A13; end; hence P[n+1]; end; A17: for n being Element of NAT holds P[n] from NAT_1:sch 1(A14,A15); A18: dom f = [:the carrier of R,NAT:] by FUNCT_2:def 1; A19: dom g = [:the carrier of R,NAT:] by FUNCT_2:def 1; now let x be set; assume x in [:the carrier of R,NAT:]; then consider v,u being set such that A20: v in the carrier of R & u in NAT & x = [v,u] by ZFMISC_1:def 2; reconsider u as Element of NAT by A20; reconsider v as Element of R by A20; thus f.x = f.(v,u) by A20 .= g.(v,u) by A17 .= g.x by A20; end; hence thesis by A18,A19,FUNCT_1:9; end; end; definition let R be non empty addLoopStr, a be Element of R, n be Element of NAT; func n * a -> Element of R equals (Nat-mult-left(R)).(n,a); coherence; func a * n -> Element of R equals (Nat-mult-right(R)).(a,n); coherence; end; theorem for R being non empty addLoopStr, a being Element of R holds 0 * a = 0.R & a * 0 = 0.R by Def6,Def7; theorem Th14: for R being right_zeroed (non empty addLoopStr), a being Element of R holds 1 * a = a proof let R be right_zeroed (non empty addLoopStr), a be Element of R; thus 1 * a = (Nat-mult-left(R)).(0+1,a) .= a + (Nat-mult-left(R)).(0,a) by Def6 .= a + 0.R by Def6 .= a by RLVECT_1:def 7; end; theorem Th15: for R being left_zeroed (non empty addLoopStr), a being Element of R holds a * 1 = a proof let R be left_zeroed (non empty addLoopStr), a be Element of R; thus a * 1 = (Nat-mult-right(R)).(a,0+1) .= (Nat-mult-right(R)).(a,0) + a by Def7 .= 0.R + a by Def7 .= a by ALGSTR_1:def 5; end; theorem Th16: for R being left_zeroed add-associative (non empty addLoopStr), a being Element of R, n,m being Element of NAT holds (n + m) * a = n * a + m * a proof let R be left_zeroed add-associative (non empty addLoopStr), a be Element of R, n,m be Element of NAT; defpred P[Element of NAT] means ($1 + m) * a = $1 * a + m * a; (0 + m) * a = 0.R + m * a by ALGSTR_1:def 5 .= 0 * a + m * a by Def6; then A1: P[0]; A2: now let k be Element of NAT; assume A3: P[k]; ((k+1) + m) * a = ((k+m) + 1) * a .= a + (k * a + m * a) by A3,Def6 .= (a + k * a) + m * a by RLVECT_1:def 6 .= (k+1) * a + m * a by Def6; hence P[k+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th17: for R being right_zeroed add-associative (non empty addLoopStr), a being Element of R, n,m being Element of NAT holds a * (n + m) = a * n + a * m proof let R be right_zeroed add-associative (non empty addLoopStr), a be Element of R, n,m be Element of NAT; defpred P[Element of NAT] means a * (n + $1) = a * n + a * $1; a * (n + 0) = a * n + 0.R by RLVECT_1:def 7 .= a * n + a * 0 by Def7; then A1: P[0]; A2: now let k be Element of NAT; assume A3: P[k]; a * (n + (k+1)) = a * ((n+k) + 1) .= (a * n + a * k) + a by A3,Def7 .= a * n + (a * k + a) by RLVECT_1:def 6 .= a * n + a * (k+1) by Def7; hence P[k+1]; end; for m being Element of NAT holds P[m] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th18: for R being left_zeroed right_zeroed add-associative (non empty addLoopStr), a being Element of R, n being Element of NAT holds n * a = a * n proof let R be left_zeroed right_zeroed add-associative (non empty addLoopStr), a be Element of R, n be Element of NAT; defpred P[Element of NAT] means $1 * a = a * $1; 0 * a = 0.R by Def6 .= a * 0 by Def7; then A1: P[0]; A2: now let k be Element of NAT; assume A3: P[k]; (k + 1) * a = k * a + 1 * a by Th16 .= k * a + a by Th14 .= a * k + a * 1 by A3,Th15 .= a * (k + 1) by Th17; hence P[k+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem for R being Abelian (non empty addLoopStr), a being Element of R, n being Element of NAT holds n * a = a * n proof let R be Abelian (non empty addLoopStr), a be Element of R, n be Element of NAT; defpred P[Element of NAT] means $1 * a = a * $1; 0 * a = 0.R by Def6 .= a * 0 by Def7; then A1: P[0]; A2: now let k be Element of NAT; assume P[k]; then (k + 1) * a = a + a * k by Def6 .= a * (k + 1) by Def7; hence P[k+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th20: for R being left_zeroed right_zeroed left_add-cancelable add-associative left-distributive (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds (n * a) * b = n * (a * b) proof let R be left_zeroed right_zeroed left_add-cancelable add-associative left-distributive (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; defpred P[Element of NAT] means ($1 * a) * b = $1 * (a * b); (0 * a) * b = 0.R * b by Def6 .= 0.R by Th1 .= 0 * (a * b) by Def6; then A1: P[0]; A2: now let k be Element of NAT; assume A3: P[k]; ((k+1) * a) * b = (a + k * a) * b by Def6 .= a * b + k * (a * b) by A3,VECTSP_1:def 12 .= 1 * (a * b) + k * (a * b) by Th14 .= (k + 1) * (a * b) by Th16; hence P[k+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th21: for R being left_zeroed right_zeroed right_add-cancelable add-associative distributive (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds b * (n * a) = (b * a) * n proof let R be left_zeroed right_zeroed add-associative right_add-cancelable distributive (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; defpred P[Element of NAT] means b * ($1 * a) = (b * a) * $1; b * (0 * a) = b * 0.R by Def6 .= 0.R by Th2 .= (b * a) * 0 by Def7; then A1: P[0]; A2: now let k be Element of NAT; assume A3: P[k]; b * ((k+1)* a) = b * (a + k * a) by Def6 .= b * a + (b * a) * k by A3,VECTSP_1:def 11 .= (b * a) * 1 + (b * a) * k by Th15 .= (b * a) * (k + 1) by Th17; hence P[k+1]; end; for n being Element of NAT holds P[n] from NAT_1:sch 1(A1,A2); hence thesis; end; theorem Th22: for R being left_zeroed right_zeroed add-associative add-cancelable distributive (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds (a * n) * b = a * (n * b) proof let R be left_zeroed right_zeroed distributive add-cancelable add-associative (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; thus (a * n) * b = (n * a) * b by Th18 .= n * (a * b) by Th20 .= (a * b) * n by Th18 .= a * (n * b) by Th21; end; begin :: The Binomial Theorem ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: definition let k,n be Element of NAT; redefine func n choose k -> Element of NAT; coherence by NEWTON:35; end; definition let R be unital (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; func (a,b) In_Power n -> FinSequence of the carrier of R means :Def10: 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 proof defpred P[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) ex y being Element of R st P[k,y] proof let k be Element of NAT; assume k in Seg(n+1); then A2: k >= 1 & k <= n+1 by FINSEQ_1:3; then reconsider m1 = k-1 as Element of NAT by INT_1:18; k-1<=n+1-1 by A2,XREAL_1:11; then reconsider l1 = n-m1 as Element of NAT by INT_1:18; reconsider z = (n choose m1) * a|^l1 * b|^m1 as Element of R; take z; thus thesis; 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 P[k,p/.k] from POLYNOM2:sch 1(A1); take p; thus thesis by A3,FINSEQ_1:def 3; end; uniqueness proof let f,g be FinSequence of the carrier of R; assume A4: 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; assume A5: 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; for i being Nat st 1 <= i & i <= len f holds f.i = g.i proof let i be Nat; assume A6: 1 <= i & i <= len f; then A7: i in Seg (n+1) by A4,FINSEQ_1:3; then A8: i in dom g by A5,FINSEQ_1:def 3; A9: i in dom f by A4,A7,FINSEQ_1:def 3; reconsider m = i-1 as Element of NAT by A6,INT_1:18; i-1<=n+1-1 by A4,A6,XREAL_1:11; then reconsider l = n-m as Element of NAT by INT_1:18; thus g.i = g/.i by A8,PARTFUN1:def 8 .= (n choose m) * a|^l * b|^m by A5,A8 .= f/.i by A4,A9 .= f.i by A9,PARTFUN1:def 8; end; hence f = g by A4,A5,FINSEQ_1:18; end; end; theorem Th23: for R being right_zeroed unital (non empty doubleLoopStr), a,b being Element of R holds (a,b) In_Power 0 = <*1_R*> proof let R be right_zeroed unital (non empty doubleLoopStr), a,b being Element of R; set p = (a,b) In_Power 0; A1: len p = 0 + 1 by Def10 .= 1; then A2: dom p = {1} by FINSEQ_1:4,def 3; then A3: 1 in dom p by TARSKI:def 1; then consider i being Element of NAT such that A4: i in dom p; A5: i = 1 by A2,A4,TARSKI:def 1; then reconsider m = i - 1 as Element of NAT by INT_1:18; reconsider l = 0 - m as Element of NAT by A5; p.1 = p/.1 by A3,PARTFUN1:def 8 .= (0 choose m) * a|^l * b|^m by A3,A5,Def10 .= 1 * a|^0 * 1_R by A5,Th8,NEWTON:27 .= 1 * 1_R * 1_R by Th8 .= 1_R * 1_R by Th14 .= 1_R by GROUP_1:def 5; hence thesis by A1,FINSEQ_1:57; end; theorem Th24: for R being right_zeroed unital (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds ((a,b) In_Power n).1 = a|^n proof let R be right_zeroed unital (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; reconsider m = 1 - 1 as Element of NAT by NEWTON:27; reconsider l = n - m as Element of NAT; len((a,b) In_Power n) = n + 1 by Def10; then A1: dom(((a,b) In_Power n)) = Seg(n + 1) by FINSEQ_1:def 3; 0 + 1 <= n + 1 by XREAL_1:8; then A2: 1 in dom(((a,b) In_Power n)) by A1,FINSEQ_1:3; hence ((a,b) In_Power n).1 = ((a,b) In_Power n)/.1 by PARTFUN1:def 8 .= (n choose 0) * a|^l * b|^m by A2,Def10 .= 1 * a|^n * b|^0 by NEWTON:29 .= a|^n * b|^0 by Th14 .= a|^n * 1_R by Th8 .= a|^n by GROUP_1:def 5; end; theorem Th25: for R being right_zeroed unital (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds ((a,b) In_Power n).(n+1) = b|^n proof let R be right_zeroed unital (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; reconsider m = n + 1 - 1 as Element of NAT; reconsider l = n - m as Element of NAT by INT_1:18; A1: l = 0; len((a,b) In_Power n) = n + 1 by Def10; then A2: dom((a,b) In_Power n) = Seg(n + 1) by FINSEQ_1:def 3; then A3: n + 1 in dom((a,b) In_Power n) by FINSEQ_1:6; thus ((a,b) In_Power n).(n+1) = ((a,b) In_Power n)/.(n+1) by A2,FINSEQ_1:6 ,PARTFUN1:def 8 .= (n choose n) * a|^0 * b|^n by A1,A3,Def10 .= 1 * a|^0 * b|^n by NEWTON:31 .= 1 * 1_R * b|^n by Th8 .= 1_R * b|^n by Th14 .= b|^n by GROUP_1:def 5; end; theorem for R being Abelian add-associative left_zeroed right_zeroed commutative associative add-cancelable distributive unital (non empty doubleLoopStr), a,b being Element of R, n being Element of NAT holds (a+b)|^n = Sum((a,b) In_Power n) proof let R be add-associative left_zeroed right_zeroed distributive associative Abelian add-cancelable commutative unital (non empty doubleLoopStr), a,b be Element of R, n be Element of NAT; defpred P[Element of NAT] means (a+b)|^$1 = Sum((a,b) In_Power $1); A1: P[0] proof thus (a+b)|^0 = 1_R by Th8 .= Sum <*1_R*> by Th3 .= Sum((a,b) In_Power 0) by Th23; end; A2: for n being Element of NAT st P[n] holds P[n+1] proof let n be Element of NAT; assume P[n]; then A3: (a+b)|^(n+1) = Sum((a,b) In_Power n) * (a + b) by GROUP_1:def 8 .= Sum((a,b) In_Power n) * a + Sum ((a,b) In_Power n) * b by VECTSP_1:def 11 .= 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; set G1 = (((a,b) In_Power n) * a)^<*0.R*>; set G2 = <*0.R*>^(((a,b) In_Power n) * b); A4: 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 3 .= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3; A5: 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 3 .= Seg(len((a,b) In_Power n)) by FINSEQ_1:def 3; len G1 = len(((a,b) In_Power n) * a) + len<*0.R*> by FINSEQ_1:35 .= len(((a,b) In_Power n) * a) + 1 by FINSEQ_1:57 .= len((a,b) In_Power n) + 1 by A4,FINSEQ_1:8 .= n + 1 + 1 by Def10; then reconsider F1 = G1 as Element of (n+1+1)-tuples_on the carrier of R by FINSEQ_2:110; len G2 = len(((a,b) In_Power n) * b) + len<*0.R*> by FINSEQ_1:35 .= len(((a,b) In_Power n) * b) + 1 by FINSEQ_1:57 .= len((a,b) In_Power n) + 1 by A5,FINSEQ_1:8 .= n + 1 + 1 by Def10; then reconsider F2 = G2 as Element of (n+1+1)-tuples_on the carrier of R by FINSEQ_2:110; A6: len F1 = n+1+1 by FINSEQ_2:109; A7: len F2 = n+1+1 by FINSEQ_2:109; A8: dom F1 = Seg(len F1) by FINSEQ_1:def 3 .= dom F2 by A6,A7,FINSEQ_1:def 3; A9: Sum F1 = Sum(((a,b) In_Power n) * a) + Sum<*0.R*> by RLVECT_1:58 .= Sum(((a,b) In_Power n) * a) + 0.R by Th3 .= Sum(((a,b) In_Power n) * a) by RLVECT_1:def 7; Sum F2 = Sum<*0.R*> + Sum(((a,b) In_Power n) * b) by RLVECT_1:58 .= 0.R + Sum(((a,b) In_Power n) * b) by Th3 .= Sum(((a,b) In_Power n) * b) by ALGSTR_1:def 5; then A10: Sum(G1+G2) = Sum(((a,b) In_Power n) * a) + Sum (((a,b) In_Power n ) * b) by A8,A9,Th7; set F = F1 + F2; A11: Seg(len F) = dom F by FINSEQ_1:def 3 .= dom F1 by A8,Def4 .= Seg(len F1) by FINSEQ_1:def 3; then A12: len F = n + 1 + 1 by A6,FINSEQ_1:8; A13: for i being Nat st 1 <= i & i <= len((a,b) In_Power (n+1)) holds F.i = ((a,b) In_Power (n+1)).i proof let i be Nat; assume A14: 1 <= i & i <= len((a,b) In_Power (n+1)); A15: len((a,b) In_Power (n+1)) = n+1+1 by Def10; then A16: dom((a,b) In_Power (n+1)) = Seg(n+1+1) by FINSEQ_1:def 3; then A17: i in dom((a,b) In_Power (n+1)) by A14,A15,FINSEQ_1:3; A18: i in Seg(n+1+1) by A14,A15,FINSEQ_1:3; reconsider j = i - 1 as Element of NAT by A14,INT_1:18; A19: i in dom F by A6,A11,A18,FINSEQ_1:def 3; A20: i in dom F1 by A6,A18,FINSEQ_1:def 3; A21: i in dom F2 by A7,A18,FINSEQ_1:def 3; A22: i = j+1; set x = ((a,b) In_Power n)/.j; set r = ((a,b) In_Power n)/.i; set r1 = F1/.i; set r2 = F2/.i; A23: i <= len(F1+F2) by A12,A14,Def10; A24: i in {1} implies F.i = ((a,b) In_Power (n+1)).i proof assume i in {1}; then A25: i = 1 by TARSKI:def 1; n+1 >= 0+1 by XREAL_1:8; then 1 in Seg (n+1) by FINSEQ_1:3; then A26: 1 in Seg len(((a,b) In_Power n)) by Def10; then A27: 1 in dom ((a,b) In_Power n) by FINSEQ_1:def 3; A28: 1 in dom (((a,b) In_Power n) * a) by A4,A26,FINSEQ_1:def 3; A29: r = ((a,b) In_Power n).i by A25,A27,PARTFUN1:def 8; A30: r1 = ((((a,b) In_Power n) * a)^<*0.R*>).1 by A20,A25,PARTFUN1:def 8 .= (((a,b) In_Power n) * a).1 by A28,FINSEQ_1:def 7 .= (((a,b) In_Power n) * a)/.1 by A28,PARTFUN1:def 8 .= (((a,b) In_Power n)/.1) * a by A27,POLYNOM1:def 3 .= a|^n * a by A25,A29,Th24 .= a|^(n+1) by GROUP_1:def 8; A31: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).1 by A21,A25,PARTFUN1:def 8 .= 0.R by FINSEQ_1:58; thus F.i = F/.i by A19,PARTFUN1:def 8 .= r1 + F2/.i by A8,A14,A23,Def4 .= a|^(n+1) by A30,A31,RLVECT_1:def 7 .= ((a,b) In_Power (n+1)).i by A25,Th24; end; A32: i in {n+1+1} implies F.i = ((a,b) In_Power (n+1)).i proof assume A33: i in {n+1+1}; then A34: i = n+1+1 by TARSKI:def 1; dom F = Seg(n+1+1) by A6,A11,FINSEQ_1:def 3; then A35: i in dom F by A14,A34,FINSEQ_1:3; A36: j = n+1+1-1 by A33,TARSKI:def 1 .= n+1; A37: n+1 = len ((a,b) In_Power n) by Def10 .= len(((a,b) In_Power n) * a) by A4,FINSEQ_1:8; n+1 in Seg (n+1) by FINSEQ_1:6; then A38: j in Seg len (((a,b) In_Power n)) by A36,Def10; then A39: j in dom ((a,b) In_Power n) by FINSEQ_1:def 3; A40: j in dom (((a,b) In_Power n) * b) by A5,A38,FINSEQ_1:def 3; A41: x = ((a,b) In_Power n).(n+1) by A36,A39,PARTFUN1:def 8 .= b|^n by Th25; A42: r1 = ((((a,b) In_Power n)*a)^<*0.R*>). (len(((a,b) In_Power n)*a)+1) by A20,A34,A37,PARTFUN1:def 8 .= 0.R by FINSEQ_1:59; A43: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(1+(n+1)) by A21,A34,PARTFUN1:def 8 .= (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> + j) by A36,FINSEQ_1:56 .= (((a,b) In_Power n) * b).j by A40,FINSEQ_1:def 7 .= (((a,b) In_Power n) * b)/.j by A40,PARTFUN1:def 8 .= b|^n * b by A39,A41,POLYNOM1:def 3 .= b|^(n+1) by GROUP_1:def 8; thus F.i = F/.i by A35,PARTFUN1:def 8 .= 0.R + r2 by A8,A14,A23,A42,Def4 .= b|^(n+1) by A43,ALGSTR_1:def 5 .= ((a,b) In_Power (n+1)).i by A34,Th25; end; A44: i in {k where k is Element of NAT: k>1 & k).i by A20,PARTFUN1:def 8; A58: r2=(<*0.R*>^(((a,b) In_Power n)*b)).i by A21,PARTFUN1:def 8; A59: r1 = (((a,b) In_Power n) * a).i by A49,A57,FINSEQ_1:def 7 .= (((a,b) In_Power n) * a)/.i by A49,PARTFUN1:def 8 .= r * a by A48,POLYNOM1:def 3; A60: r2 = (<*0.R*>^(((a,b) In_Power n) * b)).(len <*0.R*> +j) by A22,A58,FINSEQ_1:57 .= (((a,b) In_Power n) * b).j by A54,FINSEQ_1:def 7 .= (((a,b) In_Power n) * b)/.j by A56,PARTFUN1:def 8 .= x * b by A53,POLYNOM1:def 3; thus F.i = F/.i by A19,PARTFUN1:def 8 .= F1/.i + x * b by A8,A14,A23,A60,Def4 .= ((n choose m1) * a|^l1 * b|^m1) * a + x * b by A48,A59,Def10 .= (a|^l1 * (n choose m1) * b|^m1) * a + x * b by Th18 .= a * (a|^l1 *((n choose m1) * b|^m1)) + x * b by Th22 .= a * a|^l1 *((n choose m1) * b|^m1) + x * b by GROUP_1:def 4 .= a|^(l1+1) * ((n choose m1) * b|^m1) + x * b by GROUP_1:def 8 .= a|^(l1+1) * ((n choose m1) * b|^m1) + b|^m2 * ((n choose m2) * a|^l2) * b by A53,Def10 .= a|^(l1+1) * ((n choose m1) * b|^m1) + (b|^m2 * b) * ((n choose m2) * a|^l2) by GROUP_1:def 4 .= a|^(l1+1) * ((n choose (m2+1)) * b|^(m2+1)) + b|^(m2+1) * ((n choose m2) * a|^l2) by GROUP_1:def 8 .= (b|^(m2+1) * a|^(l1+1)) * (n choose (m2+1)) + b|^(m2+1) * ((n choose m2) * a|^l2) by Th21 .= b|^(m2+1) * ((n choose (m2+1)) * a|^(l1+1)) + b|^(m2+1) * ((n choose m2) * a|^l2) by Th21 .= b|^(m2+1) * (a|^(l1+1) * (n choose (m2+1))) + b|^(m2+1) * ((n choose m2) * a|^l2) by Th18 .= ((a|^(l1+1) * (n choose (m2+1))) + ((n choose m2) * a|^l2)) * b|^(m2+1) by VECTSP_1:def 18 .= (((n choose (m2+1)) * a|^(l1+1)) + ((n choose m2) * a|^(l1+1))) * b|^(m2+1) by Th18 .= ((n choose (m2+1)) + (n choose m2)) * a|^(l1+1) * b|^(m2+1) by Th16 .= ((n+1) choose (m2+1)) * a|^(l1+1) * b|^(m2+1) by NEWTON:32 .= ((a,b) In_Power (n+1))/.i by A17,A55,Def10 .= ((a,b) In_Power (n+1)).i by A17,PARTFUN1:def 8; end; now assume i in {1} \/ {k where k is Element of NAT: 1