defpred S1[ Nat] means for m being Nat
for a being Function of [:(Seg $1),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg $1 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg $1 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
reconsider n = n as Element of NAT by ORDINAL1:def 12;
now :: thesis: for m being Nat
for a being Function of [:(Seg (n + 1)),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let m be Nat; :: thesis: for a being Function of [:(Seg (n + 1)),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let a be Function of [:(Seg (n + 1)),(Seg m):],REAL; :: thesis: for p, q being FinSequence of REAL st dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let p, q be FinSequence of REAL ; :: thesis: ( dom p = Seg (n + 1) & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) implies Sum p = Sum q )
assume that
A3: dom p = Seg (n + 1) and
A4: for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) and
A5: dom q = Seg m and
A6: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg (n + 1) & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ; :: thesis: Sum p = Sum q
set a0 = a | [:(Seg n),(Seg m):];
n <= n + 1 by NAT_1:11;
then Seg n c= Seg (n + 1) by FINSEQ_1:5;
then [:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):] by ZFMISC_1:95;
then reconsider a0 = a | [:(Seg n),(Seg m):] as Function of [:(Seg n),(Seg m):],REAL by FUNCT_2:32;
deffunc H1( Nat) -> set = a . [(n + 1),$1];
reconsider p0 = p | (Seg n) as FinSequence of REAL by FINSEQ_1:18;
n + 1 in NAT by ORDINAL1:def 12;
then len p = n + 1 by A3, FINSEQ_1:def 3;
then A7: n <= len p by NAT_1:11;
then A8: dom p0 = Seg n by FINSEQ_1:17;
A9: dom p0 = Seg n by A7, FINSEQ_1:17;
A10: now :: thesis: for i being Nat st i in dom p0 holds
ex r being FinSequence of REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
let i be Nat; :: thesis: ( i in dom p0 implies ex r being FinSequence of REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) ) )
assume A11: i in dom p0 ; :: thesis: ex r being FinSequence of REAL st
( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
consider r being FinSequence of REAL such that
A12: dom r = Seg m and
A13: p . i = Sum r and
A14: for j being Nat st j in dom r holds
r . j = a . [i,j] by A3, A4, A9, A11, FINSEQ_2:8;
take r = r; :: thesis: ( dom r = Seg m & p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
thus dom r = Seg m by A12; :: thesis: ( p0 . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a0 . [i,j] ) )
thus p0 . i = Sum r by A11, A13, FUNCT_1:47; :: thesis: for j being Nat st j in dom r holds
r . j = a0 . [i,j]
thus for j being Nat st j in dom r holds
r . j = a0 . [i,j] :: thesis: verum
proof
n <= n + 1 by NAT_1:11;
then A15: Seg n c= Seg (n + 1) by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def 1;
then A16: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61
.= [:(Seg n),(Seg m):] by A15, ZFMISC_1:101 ;
let j be Nat; :: thesis: ( j in dom r implies r . j = a0 . [i,j] )
assume A17: j in dom r ; :: thesis: r . j = a0 . [i,j]
A18: [i,j] in [:(Seg n),(Seg m):] by A9, A11, A12, A17, ZFMISC_1:87;
thus r . j = a . [i,j] by A14, A17
.= a0 . [i,j] by A18, A16, FUNCT_1:47 ; :: thesis: verum
end;
end;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
consider an being FinSequence such that
A19: ( len an = m & ( for j being Nat st j in dom an holds
an . j = H1(j) ) ) from FINSEQ_1:sch 2();
A20: now :: thesis: for i being Nat st i in dom an holds
an . i in REAL
let i be Nat; :: thesis: ( i in dom an implies an . i in REAL )
assume i in dom an ; :: thesis: an . i in REAL
then an . i = a . [(n + 1),i] by A19;
hence an . i in REAL by XREAL_0:def 1; :: thesis: verum
end;
A21: dom an = Seg m by A19, FINSEQ_1:def 3;
reconsider an = an as FinSequence of REAL by A20, FINSEQ_2:12;
A22: an is Element of m -tuples_on REAL by A19, FINSEQ_2:92;
A23: dom an = Seg m by A19, FINSEQ_1:def 3;
A24: Sum an = p . (n + 1)
proof
consider r being FinSequence of REAL such that
A25: dom r = Seg m and
A26: p . (n + 1) = Sum r and
A27: for j being Nat st j in dom r holds
r . j = a . [(n + 1),j] by A3, A4, FINSEQ_1:4;
now :: thesis: for j being Nat st j in dom r holds
r . j = an . j
let j be Nat; :: thesis: ( j in dom r implies r . j = an . j )
assume A28: j in dom r ; :: thesis: r . j = an . j
hence r . j = a . [(n + 1),j] by A27
.= an . j by A19, A21, A25, A28 ;
:: thesis: verum
end;
hence Sum an = p . (n + 1) by A23, A25, A26, FINSEQ_1:13; :: thesis: verum
end;
reconsider q0 = q - an as FinSequence of REAL ;
A29: rng <:q,an:> c= [:(rng q),(rng an):] by FUNCT_3:51;
dom diffreal = [:REAL,REAL:] by FUNCT_2:def 1;
then A30: [:(rng q),(rng an):] c= dom diffreal by ZFMISC_1:96;
dom (diffreal .: (q,an)) = dom (diffreal * <:q,an:>) by FUNCOP_1:def 3
.= dom <:q,an:> by A30, A29, RELAT_1:27, XBOOLE_1:1
.= (dom q) /\ (dom an) by FUNCT_3:def 7 ;
then A31: dom q0 = (dom q) /\ (dom an) by RVSUM_1:def 6
.= (Seg m) /\ (Seg m) by A5, A19, FINSEQ_1:def 3
.= Seg m ;
then len q0 = m by FINSEQ_1:def 3;
then A32: q0 is Element of m -tuples_on REAL by FINSEQ_2:92;
A33: now :: thesis: for j being Nat st j in dom q0 holds
ex sn being FinSequence of REAL st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
let j be Nat; :: thesis: ( j in dom q0 implies ex sn being FinSequence of REAL st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) ) )
assume A34: j in dom q0 ; :: thesis: ex sn being FinSequence of REAL st
( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
consider s being FinSequence of REAL such that
A35: dom s = Seg (n + 1) and
A36: q . j = Sum s and
A37: for i being Nat st i in dom s holds
s . i = a . [i,j] by A5, A6, A31, A34;
s . (n + 1) = a . [(n + 1),j] by A35, A37, FINSEQ_1:4;
then A38: s . (n + 1) = an . j by A19, A21, A31, A34;
reconsider sn = s | (Seg n) as FinSequence of REAL by FINSEQ_1:18;
take sn = sn; :: thesis: ( dom sn = Seg n & q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
n + 1 in NAT by ORDINAL1:def 12;
then A39: len s = n + 1 by A35, FINSEQ_1:def 3;
then n <= len s by NAT_1:11;
hence A40: dom sn = Seg n by FINSEQ_1:17; :: thesis: ( q0 . j = Sum sn & ( for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] ) )
sn ^ <*(s . (n + 1))*> = s by A39, FINSEQ_3:55;
then (q . j) - (an . j) = ((Sum sn) + (an . j)) - (an . j) by A36, A38, RVSUM_1:74
.= Sum sn ;
hence q0 . j = Sum sn by A34, VALUED_1:13; :: thesis: for i being Nat st i in dom sn holds
sn . i = a0 . [i,j]
thus for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] :: thesis: verum
proof
n <= n + 1 by NAT_1:11;
then A41: Seg n c= Seg (n + 1) by FINSEQ_1:5;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def 1;
then A42: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by RELAT_1:61
.= [:(Seg n),(Seg m):] by A41, ZFMISC_1:101 ;
let i be Nat; :: thesis: ( i in dom sn implies sn . i = a0 . [i,j] )
assume A43: i in dom sn ; :: thesis: sn . i = a0 . [i,j]
A44: [i,j] in [:(Seg n),(Seg m):] by A31, A34, A40, A43, ZFMISC_1:87;
thus sn . i = s . i by A43, FUNCT_1:47
.= a . [i,j] by A35, A37, A40, A43, A41
.= a0 . [i,j] by A44, A42, FUNCT_1:47 ; :: thesis: verum
end;
end;
len q = m by A5, FINSEQ_1:def 3;
then q is Element of m -tuples_on REAL by FINSEQ_2:92;
then A45: q0 + an = q by A22, RVSUM_1:43;
n + 1 in NAT by ORDINAL1:def 12;
then len p = n + 1 by A3, FINSEQ_1:def 3;
then p0 ^ <*(Sum an)*> = p by A24, FINSEQ_3:55;
hence Sum p = (Sum p0) + (Sum an) by RVSUM_1:74
.= (Sum q0) + (Sum an) by A2, A10, A8, A31, A33
.= Sum q by A32, A22, A45, RVSUM_1:89 ;
:: thesis: verum
end;
hence S1[n + 1] ; :: thesis: verum
end;
now :: thesis: for m being Nat
for a being Function of [:(Seg 0),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let m be Nat; :: thesis: for a being Function of [:(Seg 0),(Seg m):],REAL
for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let a be Function of [:(Seg 0),(Seg m):],REAL; :: thesis: for p, q being FinSequence of REAL st dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) holds
Sum p = Sum q
let p, q be FinSequence of REAL ; :: thesis: ( dom p = Seg 0 & ( for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) ) & dom q = Seg m & ( for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ) implies Sum p = Sum q )
assume that
A46: dom p = Seg 0 and
for i being Nat st i in dom p holds
ex r being FinSequence of REAL st
( dom r = Seg m & p . i = Sum r & ( for j being Nat st j in dom r holds
r . j = a . [i,j] ) ) and
A47: dom q = Seg m and
A48: for j being Nat st j in dom q holds
ex s being FinSequence of REAL st
( dom s = Seg 0 & q . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a . [i,j] ) ) ; :: thesis: Sum p = Sum q
reconsider m = m as Element of NAT by ORDINAL1:def 12;
now :: thesis: for z being object st z in dom q holds
q . z = 0
let z be object ; :: thesis: ( z in dom q implies q . z = 0 )
assume A49: z in dom q ; :: thesis: q . z = 0
then z in { k where k is Nat : ( 1 <= k & k <= m ) } by A47, FINSEQ_1:def 1;
then ex k being Nat st
( z = k & 1 <= k & k <= m ) ;
then reconsider j = z as Nat ;
consider s being FinSequence of REAL such that
A50: dom s = Seg 0 and
A51: q . j = Sum s and
for i being Nat st i in dom s holds
s . i = a . [i,j] by A48, A49;
s = <*> REAL by A50;
hence q . z = 0 by A51, RVSUM_1:72; :: thesis: verum
end;
then q = (dom q) --> 0 by FUNCOP_1:11;
then A52: q = m |-> 0 by A47, FINSEQ_2:def 2;
p = <*> REAL by A46;
hence Sum p = Sum q by A52, RVSUM_1:72, RVSUM_1:81; :: thesis: verum
end;
then A53: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A53, A1); :: thesis: verum