:: The Binomial Theorem for Algebraic Structures
:: by Christoph Schwarzweller
::
:: Received November 20, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, RLVECT_1, ALGSTR_0, XBOOLE_0, SUBSET_1, ARYTM_3,
ALGSTR_1, BINOP_1, LATTICES, GROUP_1, VECTSP_2, VECTSP_1, SUPINF_2,
RELAT_1, FUNCT_1, ZFMISC_1, CARD_1, FUNCT_2, MCART_1, CARD_3, FINSEQ_1,
STRUCT_0, XXREAL_0, PARTFUN1, NAT_1, NEWTON, ARYTM_1, ORDINAL4, FINSEQ_2,
BINOM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
STRUCT_0, ALGSTR_0, PARTFUN1, FUNCT_1, FUNCT_2, FINSEQ_1, RELSET_1,
BINOP_1, NAT_1, ALGSTR_1, FINSEQ_2, VECTSP_1, VECTSP_2, GROUP_1, NEWTON,
RLVECT_1, XTUPLE_0, MCART_1, POLYNOM1, XXREAL_0;
constructors BINOP_1, REAL_1, NEWTON, ALGSTR_1, MONOID_0, POLYNOM1, RELSET_1,
FVSUM_1, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
FINSEQ_2, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, INT_1, ALGSTR_0,
CARD_1, FINSEQ_1, XTUPLE_0;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
definitions ALGSTR_0;
equalities BINOP_1, ALGSTR_0;
theorems TARSKI, FUNCT_2, VECTSP_1, RLVECT_1, ALGSTR_1, NAT_1, FINSEQ_1,
GROUP_1, NEWTON, FINSEQ_2, FUNCT_1, ZFMISC_1, INT_1, POLYNOM1, XBOOLE_0,
XREAL_1, PARTFUN1, ORDINAL1, ALGSTR_0, CARD_1, FINSEQ_5, XTUPLE_0;
schemes NAT_1, RECDEF_1, INT_1;
begin :: Preliminaries
registration
cluster Abelian right_add-cancelable -> left_add-cancelable for 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 thesis by ALGSTR_0:def 4;
end;
hence thesis;
end;
cluster Abelian left_add-cancelable -> right_add-cancelable for 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 thesis by ALGSTR_0:def 3;
end;
hence thesis;
end;
end;
registration
cluster right_zeroed right_complementable add-associative ->
right_add-cancelable for non empty addLoopStr;
coherence;
end;
registration
cluster Abelian add-associative left_zeroed right_zeroed commutative
associative add-cancelable distributive unital for
non empty doubleLoopStr;
existence
proof
set R = the 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 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 thesis 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 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 thesis by ALGSTR_0:def 4;
end;
Lm1:
now
let C,D be non empty set, b be Element of D, F be Function of [:C,D:],D;
thus ex g being Function of [:NAT,C:],D st for a being Element of C holds
g.(0,a) = b & for n being Nat holds g.(n+1,a) = F.(a,g.(n,a))
proof
A1: for a being Element of C holds ex f being sequence of D st f.0 =
b & for n being Nat holds f.(n+1) = F.(a,f.n)
proof
let a be Element of C;
defpred P[Nat,Element of D,Element of D] means $3 = F.(a,$2);
A2: for n being Nat for x being Element of D ex y being
Element of D st P[n,x,y];
ex f being sequence of D st f.0 = b &
for n being 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 sequence of D st g.a = f & f.0 = b & for n being
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 sequence of D st f = l & f.0 = b &
for n being Nat holds f.(n+1) = F.(a,f.n) };
A3: now
let x,y1,y2 be object;
assume that
A4: [x,y1] in h and
A5: [x,y2] in h;
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 sequence of D st f = l1 & f.0 = b & for n
being 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 sequence of D st f = l2 & f.0 = b & for n
being Nat holds f.(n+1) = F.(a2,f.n) by A5;
consider f1 being sequence of D such that
A10: f1 = l1 and
A11: f1.0 = b and
A12: for n being Nat holds f1.(n+1) = F.(a1,f1.n) by A7;
consider f2 being sequence of D such that
A13: f2 = l2 and
A14: f2.0 = b and
A15: for n being 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
defpred P[Nat] means f1.$1 = f2.$1;
let x be object;
assume x in NAT;
then reconsider x9 = x as Element of NAT;
A18: now
let n be Nat;
assume
A19: P[n];
f1.(n+1) = F.(a2,f1.n) by A12,A16
.= f2.(n+1) by A15,A19;
hence P[n+1];
end;
A20: P[0] by A11,A14;
for n being Nat holds P[n] from NAT_1:sch 2(A20,A18);
hence f1.x = f2.x9 .= f2.x;
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;
end;
now
let x be object;
assume x in h;
then ex a being Element of C, l being Element of Funcs(NAT,D) st x =
[a,l] & ex f being sequence of D st f = l & f.0 = b & for n being
Nat holds f.(n+1) = F.(a,f.n);
hence x in [:C,Funcs(NAT,D):] by ZFMISC_1:def 2;
end;
then reconsider h as Relation of C,Funcs(NAT,D) by TARSKI:def 3;
A22: for x being object holds x in C implies x in dom h
proof
let x be object;
assume
A23: x in C;
then consider f being sequence of D such that
A24: f.0 = b & for n being Nat holds f.(n+1) = F.(x,f.n) by A1;
f in Funcs(NAT,D) by FUNCT_2:8;
then [x,f] in h by A23,A24;
hence thesis by XTUPLE_0:def 12;
end;
for x being object holds x in dom h implies x in C;
then dom h = C by A22,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 sequence of D st h.
a = f & f.0 = b & for n being 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: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 sequence of D st f9 = l & f9.0 = b & for n
being 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 thesis by A26,A27;
end;
hence thesis;
end;
then consider g being Function of C,Funcs(NAT,D) such that
A28: for a being Element of C holds ex f being sequence of D st
g.a = f & f.0 = b & for n being 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 sequence of D st f = g.a & z = f.n };
A29: now
let x,y1,y2 be object;
assume that
A30: [x,y1] in h and
A31: [x,y2] in h;
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 sequence of 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 sequence of 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;
end;
now
let x be object;
assume x in h;
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 sequence of 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;
end;
then reconsider h as Relation of [:NAT,C:],D by TARSKI:def 3;
A40: for x being object holds x in [:NAT,C:] implies x in dom h
proof
let x be object;
assume x in [:NAT,C:];
then consider n,d being object such that
A41: n in NAT and
A42: d in C and
A43: x = [n,d] by ZFMISC_1:def 2;
reconsider d as Element of C by A42;
reconsider n as Element of NAT by A41;
consider f9 being sequence of D such that
A44: g.d = f9 and
f9.0 = b and
for n being Nat holds f9.(n+1) = F.(d,f9.n) by A28;
ex z being Element of D st ex f being sequence of D st f = g.
d & z = f.n
proof
take f9.n;
take f9;
thus thesis by A44;
end;
then consider z being Element of D such that
A45: ex f being sequence of D st f = g.d & z = f.n;
[x,z] in h by A43,A45;
hence thesis by XTUPLE_0:def 12;
end;
for x being object holds x in dom h implies x in [:NAT,C:];
then dom h = [:NAT,C:] by A40,TARSKI:2;
then reconsider h as Function of [:NAT,C:],D by A29,FUNCT_1:def 1
,FUNCT_2:def 1;
take h;
for a being Element of C holds h.(0,a) = b & for n being Nat
holds h.(n+1,a) = F.(a,h.(n,a))
proof
let a be Element of C;
consider f9 being sequence of D such that
A46: g.a = f9 and
A47: f9.0 = b and
A48: for n being Nat holds f9.(n+1) = F.(a,f9.n) by A28;
A49: now
let k be 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 object such that
A50: [[k+1,a],u] in h by XTUPLE_0:def 12;
k in NAT by ORDINAL1:def 12;
then [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 object 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 sequence of 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 sequence of 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;
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 object 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 sequence of 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 thesis by A46,A47,A63,A65,A66,A68,A49,FUNCT_1:1;
end;
hence thesis;
end;
end;
Lm2:
now let C,D be non empty set, b be Element of D, F be Function of [:D,C:],D;
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) proof
A1: for a being Element of C holds ex f being sequence of D st f.0 =
b & for n being Nat holds f.(n+1) = F.(f.n,a)
proof
let a be Element of C;
defpred P[Nat,Element of D,Element of D] means $3 = F.($2
,a);
A2: for n being Nat for x being Element of D ex y being
Element of D st P[n,x,y];
ex f being sequence of D st f.0 = b &
for n being 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 sequence of D st g.a = f & f.0 = b & for n being
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 sequence of D st f = l & f.0 = b &
for n being Nat holds f.(n+1) = F.(f.n,a) };
A3: now
let x,y1,y2 be object;
assume that
A4: [x,y1] in h and
A5: [x,y2] in h;
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 sequence of D st f = l1 & f.0 = b & for n
being 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 sequence of D st f = l2 & f.0 = b & for n
being Nat holds f.(n+1) = F.(f.n,a2) by A5;
consider f1 being sequence of D such that
A10: f1 = l1 and
A11: f1.0 = b and
A12: for n being Nat holds f1.(n+1) = F.(f1.n,a1) by A7;
consider f2 being sequence of D such that
A13: f2 = l2 and
A14: f2.0 = b and
A15: for n being 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
defpred P[Nat] means f1.$1 = f2.$1;
let x be object;
assume x in NAT;
then reconsider x9 = x as Element of NAT;
A18: now
let n be Nat;
assume
A19: P[n];
f1.(n+1) = F.(f1.n,a2) by A12,A16
.= f2.(n+1) by A15,A19;
hence P[n+1];
end;
A20: P[0] by A11,A14;
for n being Nat holds P[n] from NAT_1:sch 2(A20,A18 );
hence f1.x = f2.x9 .= f2.x;
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;
end;
now
let x be object;
assume x in h;
then ex a being Element of C, l being Element of Funcs(NAT,D) st x =
[a,l] & ex f being sequence of D st f = l & f.0 = b & for n being
Nat holds f.(n+1) = F.(f.n,a);
hence x in [:C,Funcs(NAT,D):] by ZFMISC_1:def 2;
end;
then reconsider h as Relation of C,Funcs(NAT,D) by TARSKI:def 3;
A22: for x being object holds x in C implies x in dom h
proof
let x be object;
assume
A23: x in C;
then consider f being sequence of D such that
A24: f.0 = b & for n being Nat holds f.(n+1) = F.(f.n,x) by A1;
reconsider f9 = f as Element of Funcs(NAT,D) by FUNCT_2:8;
f in Funcs(NAT,D) by FUNCT_2:8;
then [x,f] in h by A23,A24;
hence thesis by XTUPLE_0:def 12;
end;
for x being object holds x in dom h implies x in C;
then dom h = C by A22,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 sequence of D st h.
a = f & f.0 = b & for n being 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: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 sequence of D st f9 = l & f9.0 = b & for n
being 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 thesis by A26,A27;
end;
hence thesis;
end;
then consider g being Function of C,Funcs(NAT,D) such that
A28: for a being Element of C holds ex f being sequence of D st
g.a = f & f.0 = b & for n being 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 sequence of D st f = g.a & z = f.n };
A29: now
let x,y1,y2 be object;
assume that
A30: [x,y1] in h and
A31: [x,y2] in h;
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 sequence of 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 sequence of 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;
end;
now
let x be object;
assume x in h;
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 sequence of 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;
end;
then reconsider h as Relation of [:C,NAT:],D by TARSKI:def 3;
A40: for x being object holds x in [:C,NAT:] implies x in dom h
proof
let x be object;
assume x in [:C,NAT:];
then consider d,n being object such that
A41: d in C and
A42: n in NAT and
A43: x = [d,n] by ZFMISC_1:def 2;
reconsider d as Element of C by A41;
reconsider n as Element of NAT by A42;
consider f9 being sequence of D such that
A44: g.d = f9 and
f9.0 = b and
for n being Nat holds f9.(n+1) = F.(f9.n,d) by A28;
ex z being Element of D st ex f being sequence of D st f = g.
d & z = f.n
proof
take f9.n;
take f9;
thus thesis by A44;
end;
then consider z being Element of D such that
A45: ex f being sequence of D st f = g.d & z = f.n;
[x,z] in h by A43,A45;
hence thesis by XTUPLE_0:def 12;
end;
for x being object holds x in dom h implies x in [:C,NAT:];
then dom h = [:C,NAT:] by A40,TARSKI:2;
then reconsider h as Function of [:C,NAT:],D by A29,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 f9 being sequence of D such that
A46: g.a = f9 and
A47: f9.0 = b and
A48: for n being Nat holds f9.(n+1) = F.(f9.n,a) by A28;
A49: 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 object 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 object 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 sequence of 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 sequence of 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 sequence of 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;
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 object 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 sequence of 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 thesis by A46,A47,A65,A67,A68,A70,A49,FUNCT_1:1;
end;
hence thesis;
end;
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 sequence of the carrier of V such that
A1: Sum(S) = f.(len S) and
A2: f.0 = 0.V & for j being 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 12;
A3: len <* a *> = 1 by FINSEQ_1:39;
0 < 1;
then consider j being Element of NAT such that
A4: j < len S;
A5: S.(j + 1) = S.(0 + 1) by A3,A4,NAT_1:14
.= v;
j = 0 by A3,A4,NAT_1:14;
then f.1 = 0.V + v by A2,A5
.= a by ALGSTR_1:def 2;
hence thesis by A1,FINSEQ_1:39;
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 sequence of the carrier of R such that
A1: Sum p = f.(len p) and
A2: f.0 = 0.R and
A3: for j being 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 12;
consider fa being sequence of 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 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 12;
defpred P[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
let j be Element of NAT;
assume that
0 <= j and
A9: j < len p;
thus P[j] implies P[j+1]
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 P[j];
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;
end;
end;
A15: P[0] by A2,A5,Th2;
A16: for i being Element of NAT st 0 <= i & i <= len p holds P[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;
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 sequence of the carrier of R such that
A1: Sum p = f.(len p) and
A2: f.0 = 0.R and
A3: for j being 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 12;
consider fa being sequence of 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 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 12;
defpred P[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
let j be Element of NAT;
assume that
0 <= j and
A9: j < len p;
thus P[j] implies P[j+1]
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;
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;
end;
end;
A16: P[0] by A2,A5,Th1;
A17: for i being Element of NAT st 0 <= i & i <= len p holds P[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;
end;
theorem
for R being commutative non empty multMagma, a being Element of R,
p being FinSequence of the carrier of R holds p * a = a * p
proof
let R be commutative non empty multMagma, a be Element of R, p be
FinSequence of the carrier of R;
set pa = p*a, ap = a*p;
A1: dom pa = dom p by POLYNOM1:def 2;
A2: dom ap = dom p by POLYNOM1:def 1;
now
let i be Nat such that
A3: i in dom pa;
thus pa/.i = p/.i * a by A1,A3,POLYNOM1:def 2
.= ap/.i by A1,A3,POLYNOM1:def 1;
end;
hence thesis by A1,A2,FINSEQ_5:12;
end;
definition
let R be non empty addLoopStr, p,q be FinSequence of the carrier of R;
func p + q -> FinSequence of the carrier of R means
:Def1:
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[Nat,Element of R] means $2 = (p/.($1)) + (q/.($1));
A1: for k being 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 Nat st k in Seg(len p)
holds P[k,f/.k] from RECDEF_1:sch 17(A1);
take f;
A3: len f = len p by A2,FINSEQ_1:def 3;
for m being Nat st 1 <= m <= len f holds f/.m = p/.m + q/.m
by A2,A3,FINSEQ_1:1;
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 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;
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
let i be Nat;
assume
A10: 1 <= i & i <= len y1;
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;
end;
hence thesis by A8,FINSEQ_1:6,14;
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;
consider fp being sequence of the carrier of R such that
A1: Sum p = fp.(len p) and
A2: fp.0 = 0.R and
A3: for j being 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 12;
consider fq being sequence of the carrier of R such that
A4: Sum q = fq.(len q) and
A5: fq.0 = 0.R and
A6: for j being 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 12;
assume dom p = dom 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 sequence of 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 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 12;
defpred P[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
let j be Element of NAT;
assume that
0 <= j and
A15: j < len p;
thus P[j] implies P[j+1]
proof
assume
A16: P[j];
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 thesis;
end;
end;
A22: P[0] by A2,A5,A10,RLVECT_1:def 4;
A23: for i being Element of NAT st 0 <= i & i <= len p holds P[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;
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;
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 7;
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 thesis;
end;
theorem
for R being unital associative commutative non empty multMagma,
a,b being Element of R, n being 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 Nat;
defpred P[Nat] means power(R).(a * b,$1) = a|^$1 * b|^$1;
A1: now
let m be Nat;
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
assume P[m];
then
power(R).(a * b,m+1) = (power(R).(a,mm) * power(R).(b,mm)) * (a * b) by
GROUP_1:def 7
.= ((power(R).(a,mm) * power(R).(b,mm)) * a) * b by GROUP_1:def 3
.= ((power(R).(a,mm) * a) * power(R).(b,mm)) * b by GROUP_1:def 3
.= (power(R).(a,mm) * a) * (power(R).(b,mm) * b) by GROUP_1:def 3
.= (a|^(m+1)) * (power(R).(b,mm) * b) by GROUP_1:def 7
.= (a|^(m+1)) * (b|^(m+1)) by GROUP_1:def 7;
hence P[m+1];
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
A2: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
Lm3:
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[Nat] means power(R).(a,n+$1) = power(R).(a,n) * a|^$1;
A1: now
let m be Nat;
assume
A2: P[m];
reconsider mm=m as Element of NAT by ORDINAL1:def 12;
power(R).(a,n+(m+1)) = power(R).(a,(n+m)+1)
.= (power(R).(a,n) * power(R).(a,mm)) * a by A2,GROUP_1:def 7
.= power(R).(a,n) * (power(R).(a,mm) * a) by GROUP_1:def 3
.= power(R).(a,n) * a|^(m+1) by GROUP_1:def 7;
hence P[m+1];
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: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th10:
for R being unital associative non empty multMagma,
a being Element of R, n,m being 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 Nat;
reconsider n1 = n, m1 = m as Element of NAT by ORDINAL1:def 12;
a|^(n1+m1) = (a|^n1) * (a|^m1) by Lm3;
hence thesis;
end;
theorem
for R being unital associative non empty multMagma, a being Element
of R, n,m being 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
Nat;
defpred P[Nat] means power(R).(a|^n,$1) = power(R).(a,n * $1);
A1: now
let m be Nat;
assume P[m];
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 P[m+1];
end;
power(R).(a|^n,0) = 1_R by GROUP_1:def 7
.= power(R).(a,n * 0) by GROUP_1:def 7;
then
A2: P[0];
for k being Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
begin :: On 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
:Def3:
for a being Element of R holds it.(0,a) = 0.R &
for n being 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 Nat holds g.(n+1,a) = (the addF of R).(a,g.(n,a)) by Lm1;
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 Nat holds f.(n+1,a) = a + f.(n,a);
defpred P[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 Nat holds g.(n+1,a) = a + g.(n,a);
A4: now
let n be Nat;
assume
A5: P[n];
now
let a be Element of R;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus f.(n+1,a) = a + f.(nn,a) by A2
.= a + g.(nn,a) by A5
.= g.(n+1,a) by A3;
end;
hence P[n+1];
end;
A6: P[0]
proof
let a be Element of R;
thus f.(0,a) = 0.R by A2
.= g.(0,a) by A3;
end;
A7: for n being Nat holds P[n] from NAT_1:sch 2(A6,A4);
A8: now
let x be object;
assume x in [:NAT,the carrier of R:];
then consider u,v being object 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 as Element of R by A10;
reconsider u as Element of NAT by A9;
thus f.x = f.(u,v) by A11
.= g.(u,v) by A7
.= g.x by A11;
end;
dom f = [:NAT,the carrier of R:] & dom g = [:NAT,the carrier of R:] by
FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:2;
end;
func Nat-mult-right(R) -> Function of [:the carrier of R,NAT:],the carrier
of R means
:Def4:
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
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;
thus thesis by A12;
end;
uniqueness
proof
let f,g be Function of [:the carrier of R,NAT:],the carrier of R;
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;
defpred P[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;
A15: now
let n be Nat;
assume
A16: P[n];
now
let a be Element of R;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
thus f.(a,n+1) = f.(a,nn) + a by A13
.= g.(a,nn) + a by A16
.= g.(a,n+1) by A14;
end;
hence P[n+1];
end;
A17: P[0]
proof
let a be Element of R;
thus f.(a,0) = 0.R by A13
.= g.(a,0) by A14;
end;
A18: for n being Nat holds P[n] from NAT_1:sch 2(A17,A15);
A19: now
let x be object;
assume x in [:the carrier of R,NAT:];
then consider v,u being object 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 as Element of R by A20;
reconsider u as Element of NAT by A21;
thus f.x = f.(v,u) by A22
.= g.(v,u) by A18
.= g.x by A22;
end;
dom f = [:the carrier of R,NAT:] & dom g = [:the carrier of R,NAT:]
by FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:2;
end;
end;
definition
let R be non empty addLoopStr, a be Element of R, n be 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 Def3,Def4;
theorem Th13:
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 Def3
.= a + 0.R by Def3
.= a by RLVECT_1:def 4;
end;
theorem Th14:
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 Def4
.= 0.R + a by Def4
.= a by ALGSTR_1:def 2;
end;
theorem Th15:
for R being left_zeroed add-associative non empty addLoopStr,
a being Element of R, n,m being 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 Nat;
defpred P[Nat] means ($1 + m) * a = $1 * a + m * a;
A1: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A2: P[k];
(k+1 + m) * a = (k+m + 1) * a
.= a + (k+m)*a by Def3
.= a + (kk * a + m * a) by A2
.= (a + k * a) + m * a by RLVECT_1:def 3
.= (kk+1) * a + m * a by Def3;
hence P[k+1];
end;
(0 + m) * a = 0.R + m * a by ALGSTR_1:def 2
.= 0 * a + m * a by Def3;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th16:
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[Nat] means a * (n + $1) = a * n + a * $1;
A1: now
let k be Nat;
assume
A2: P[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
a * (n + (k+1)) = a * ((n+kk) + 1) .= (a * n + a * kk) + a by A2,Def4
.= a * n + (a * k + a) by RLVECT_1:def 3
.= a * n + a * (kk+1) by Def4;
hence P[k+1];
end;
a * (n + 0) = a * n + 0.R by RLVECT_1:def 4
.= a * n + a * 0 by Def4;
then
A3: P[0];
for m being Nat holds P[m] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th17:
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[Nat] means $1 * a = a * $1;
A1: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A2: P[k];
(kk + 1) * a = k * a + 1 * a by Th15
.= k * a + a by Th13
.= a * k + a * 1 by A2,Th14
.= a * (kk + 1) by Th16;
hence P[k+1];
end;
0 * a = 0.R by Def3
.= a * 0 by Def4;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
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[Nat] means $1 * a = a * $1;
A1: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume P[k];
then (kk + 1) * a = a + a * k by Def3
.= a * (kk + 1) by Def4;
hence P[k+1];
end;
0 * a = 0.R by Def3
.= a * 0 by Def4;
then
A2: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
theorem Th19:
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[Nat] means ($1 * a) * b = $1 * (a * b);
A1: now
let k be Nat;
assume
A2: P[k];
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
((kk+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
.= (kk + 1) * (a * b) by Th15;
hence P[k+1];
end;
(0 * a) * b = 0.R * b by Def3
.= 0.R by Th1
.= 0 * (a * b) by Def3;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th20:
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[Nat] means b * ($1 * a) = (b * a) * $1;
A1: now
let k be Nat;
reconsider kk=k as Element of NAT by ORDINAL1:def 12;
assume
A2: P[k];
b * ((kk+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) * (kk + 1) by Th16;
hence P[k+1];
end;
b * (0 * a) = b * 0.R by Def3
.= 0.R by Th2
.= (b * a) * 0 by Def4;
then
A3: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
hence thesis;
end;
theorem Th21:
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 Th17
.= n * (a * b) by Th19
.= (a * b) * n by Th17
.= a * (n * b) by Th20;
end;
begin :: The Binomial Theorem
definition
let R be unital non empty doubleLoopStr, a,b be Element of R, n be Nat;
func (a,b) In_Power n -> FinSequence of the carrier of R means
:Def7:
len it = n + 1 & for i,l,m being 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[Nat,Element of R] means for l,m being Nat
st m = $1 - 1 & l = n - m holds $2 = (n choose m) * a|^l * b|^m;
A1: for k being Nat st k in Seg(n+1) ex y being Element of R st P[k,y]
proof
let k be Nat;
assume
A2: k in Seg(n+1);
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;
thus thesis;
end;
consider p being FinSequence of the carrier of R such that
A3: dom p = Seg(n+1) & for k being Nat st k in Seg(n+1)
holds P[k,p/.k] from RECDEF_1:sch 17(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 that
A4: len f = n + 1 and
A5: for i,l,m being Nat st i in dom f & m = i - 1 & l = n -
m holds f/.i = (n choose m) * a|^l * b|^m;
assume that
A6: len g = n + 1 and
A7: for i,l,m being 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 that
A8: 1 <= i and
A9: i <= len f;
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;
end;
hence f = g by A4,A6,FINSEQ_1:14;
end;
end;
theorem Th22:
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 Def7
.= 1;
then
A2: dom p = {1} by FINSEQ_1:2,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:5;
reconsider l = 0 - m as Element of NAT by A5;
p.1 = p/.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 thesis by A1,FINSEQ_1:40;
end;
theorem Th23:
for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R, n being 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 right_zeroed unital non empty doubleLoopStr, a,b be Element of R,
n be Nat;
reconsider l = n - m as 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;
end;
theorem Th24:
for R being right_zeroed unital non empty doubleLoopStr, a,b
being Element of R, n being 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 Nat;
reconsider m = n + 1 - 1 as 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;
end;
::$N Binomial Theorem
::$L https://en.wikipedia.org/wiki/Binomial_theorem Binomial Theorem
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[Nat] means (a+b)|^$1 = Sum((a,b) In_Power $1);
A1: for n being Nat st P[n] holds P[n+1]
proof
let n be Nat;
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 G1 = 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 = G1 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 G2 = 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 = G2 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 F) = dom F by FINSEQ_1:def 3
.= dom F1 by Def1
.= Seg(len F1) by FINSEQ_1:def 3;
then
A7: len F = 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 F.i
= ((a,b) In_Power (n+1)).i
proof
let i be Nat;
assume that
A9: 1 <= i and
A10: i <= len((a,b) In_Power (n+1));
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 F.i = ((a,b) In_Power (n+1)).i
proof
assume
A20: i in {n+1+1};
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: r1 = ((((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: x = ((a,b) In_Power n).(n+1) by A23,PARTFUN1:def 6
.= b|^n by Th24;
A28: r2 = (<*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 F = Seg(n+1+1) by A4,A6,FINSEQ_1:def 3;
then i in dom F by A9,A21,FINSEQ_1:1;
hence F.i = F/.i by PARTFUN1:def 6
.= 0.R + r2 by A9,A18,A22,Def1
.= b|^(n+1) by A28,ALGSTR_1:def 2
.= ((a,b) In_Power (n+1)).i by A21,Th24;
end;
A29: i in dom F 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 F.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};
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;
r2=(<*0.R*>^(((a,b) In_Power n)*b)).i by A17,PARTFUN1:def 6;
then
A40: r2 = (<*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
.= x * 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;
r1=((((a,b) In_Power n)*a)^<*0.R*>).i by A16,PARTFUN1:def 6;
then
A43: r1 = (((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
.= r * a by A34,POLYNOM1:def 2;
thus F.i = F/.i by A29,PARTFUN1:def 6
.= F1/.i + x * b by A9,A18,A40,Def1
.= ((n choose m1) * a|^l1 * b|^m1) * a + x * b by A34,A43,Def7
.= (a|^l1 * (n choose m1) * b|^m1) * a + x * b by Th17
.= a * (a|^l1 *((n choose m1) * b|^m1)) + x * b by Th21
.= a * a|^l1 *((n choose m1) * b|^m1) + x * b by GROUP_1:def 3
.= a|^(l1+1) * ((n choose m1) * b|^m1) + x * 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;
end;
A44: i in {1} implies F.i = ((a,b) In_Power (n+1)).i
proof
assume i in {1};
then
A45: i = 1 by TARSKI:def 1;
then
A46: r2 = (<*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: r = ((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: r1 = ((((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 F.i = F/.i by A29,PARTFUN1:def 6
.= r1 + 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;
end;
now
assume
i in {1} \/ {k where k is Element of NAT: 1<k & k<n+1+1} \/ { n+1+1};
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 thesis by A44,A19,A30,XBOOLE_0:def 3;
end;
hence thesis by A12,A13,NAT_1:12,NEWTON:1;
end;
assume P[n];
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(G1+G2) = 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 F by A7,Def7;
hence thesis by A52,A55,A8,FINSEQ_1:14;
end;
(a+b)|^0 = 1_R by Th8
.= Sum <*1_R*> by Th3
.= Sum((a,b) In_Power 0) by Th22;
then
A56: P[0];
for n being Nat holds P[n] from NAT_1:sch 2(A56,A1);
hence thesis;
end;
theorem
for C,D be non empty set, b be Element of D, F be 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 Nat holds g.(n+1,a) = F.(a,g.(n,a))
by Lm1;
theorem
for C,D be non empty set, b be Element of D, F be 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;