defpred S₁[ 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 S₁[n] holds
S₁[n + 1]

let m be Nat; :: thesis:
let a be Function of [:(Seg (n + 1)),(Seg m):],REAL; :: thesis:
let p, q be FinSequence of REAL ; :: thesis:
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:
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 H₁( 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;

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 = H₁(j) ) ) from FINSEQ_1:sch 2();

end;

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;

let j be Nat; :: thesis:
assume A28: j in dom r ; :: thesis:
hence r . j = a . [(n + 1),j] by A27
.= an . j by A19, A21, A25, A28 ;
:: thesis:

end;

end;

let j be Nat; :: thesis:
assume A34: j in dom q0 ; :: thesis:
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:
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:
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:
thus for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] :: thesis:

end;

end;

hence S₁[n + 1] ; :: thesis:

end;

let m be Nat; :: thesis:
let a be Function of [:(Seg 0),(Seg m):],REAL; :: thesis:
let p, q be FinSequence of REAL ; :: thesis:
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:
reconsider m = m as Element of NAT by ORDINAL1:def 12;

let z be object ; :: thesis:
assume A49: z in dom q ; :: thesis:
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:

end;

end;