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: S₁[ 0 ]

proof

now

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
A2: 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
A3: dom q = Seg m and
A4: 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 13;
thus Sum p = Sum q :: thesis:

proof

len p = 0 by A2, FINSEQ_1:def 3;
then A5: Sum p = 0 by FINSEQ_1:32, RVSUM_1:102;
q = (dom q) --> 0

proof

now

let z be set ; :: thesis:
assume A6: z in dom q ; :: thesis:
then z in { k where k is Element of NAT : ( 1 <= k & k <= m ) } by A3, FINSEQ_1:def 1;
then consider k being Element of NAT such that
A7: ( z = k & 1 <= k & k <= m ) ;
reconsider j = z as Nat by A7;
consider s being FinSequence of REAL such that
A8: dom s = Seg 0 and
A9: q . j = Sum s and
for i being Nat st i in dom s holds
s . i = a . [i,j] by A4, A6;
len s = 0 by A8, FINSEQ_1:def 3;
hence q . z = 0 by A9, FINSEQ_1:32, RVSUM_1:102; :: thesis:

end;

hence q = (dom q) --> 0 by FUNCOP_1:17; :: thesis:

end;

then q = m |-> 0 by A3, FINSEQ_2:def 2;
hence Sum p = Sum q by A5, RVSUM_1:111; :: thesis:

end;

hence S₁[ 0 ] ; :: thesis:

end;

A10: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A11: S₁[n] ; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;

now

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
A12: ( 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] ) ) ) ) and
A13: ( 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] ) ) ) ) ; :: 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:7;
then [:(Seg n),(Seg m):] c= [:(Seg (n + 1)),(Seg m):] by ZFMISC_1:118;
then reconsider a0 = a | [:(Seg n),(Seg m):] as Function of [:(Seg n),(Seg m):], REAL by FUNCT_2:38;
reconsider p0 = p | (Seg n) as FinSequence of REAL by FINSEQ_1:23;
A14: ( dom p0 = Seg n & ( 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] ) ) ) )

proof

len p = n + 1 by A12, FINSEQ_1:def 3;
then n <= len p by NAT_1:11;
hence A15: dom p0 = Seg n by FINSEQ_1:21; :: thesis:

now

let i be Nat; :: thesis:
assume A16: i in dom p0 ; :: thesis:
i in dom p by A12, A15, A16, FINSEQ_2:9;
then consider r being FinSequence of REAL such that
A17: dom r = Seg m and
A18: p . i = Sum r and
A19: for j being Nat st j in dom r holds
r . j = a . [i,j] by A12;
take r = r; :: thesis:
thus dom r = Seg m by A17; :: thesis:
thus p0 . i = Sum r by A16, A18, FUNCT_1:70; :: thesis:
thus for j being Nat st j in dom r holds
r . j = a0 . [i,j] :: thesis:

proof

let j be Nat; :: thesis:
assume A20: j in dom r ; :: thesis:
A21: [i,j] in [:(Seg n),(Seg m):] by A15, A16, A17, A20, ZFMISC_1:106;
n <= n + 1 by NAT_1:11;
then A22: Seg n c= Seg (n + 1) by FINSEQ_1:7;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def 1;
then A23: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by FUNCT_1:68
.= [:(Seg n),(Seg m):] by A22, ZFMISC_1:124 ;
thus r . j = a . [i,j] by A19, A20
.= a0 . [i,j] by A21, A23, FUNCT_1:70 ; :: thesis:

end;

hence 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] ) ) ; :: thesis:

end;

deffunc H₁( Nat) -> Element of REAL = a . [(n + 1),$1];
reconsider m = m as Element of NAT by ORDINAL1:def 13;
consider an being FinSequence such that
A24: ( len an = m & ( for j being Nat st j in dom an holds
an . j = H₁(j) ) ) from FINSEQ_1:sch 2();
A25: dom an = Seg m by A24, FINSEQ_1:def 3;
an is FinSequence of REAL

proof

now

let i be Nat; :: thesis:
assume i in dom an ; :: thesis:
then i in Seg m by A24, FINSEQ_1:def 3;
then an . i = a . [(n + 1),i] by A24, A25;
hence an . i in REAL ; :: thesis:

end;

hence an is FinSequence of REAL by FINSEQ_2:14; :: thesis:

end;

then reconsider an = an as FinSequence of REAL ;
A26: dom an = Seg m by A24, FINSEQ_1:def 3;
A27: Sum an = p . (n + 1)

proof

n + 1 in dom p by A12, FINSEQ_1:6;
then consider r being FinSequence of REAL such that
A28: dom r = Seg m and
A29: p . (n + 1) = Sum r and
A30: for j being Nat st j in dom r holds
r . j = a . [(n + 1),j] by A12;

now

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

end;

hence Sum an = p . (n + 1) by A26, A28, A29, FINSEQ_1:17; :: thesis:

end;

reconsider q0 = q - an as FinSequence of REAL ;
A32: ( dom q0 = Seg m & ( for j being Nat st j in dom q0 holds
ex s being FinSequence of REAL st
( dom s = Seg n & q0 . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a0 . [i,j] ) ) ) )

proof

dom diffreal = [:REAL ,REAL :] by FUNCT_2:def 1;
then A33: [:(rng q),(rng an):] c= dom diffreal by ZFMISC_1:119;
A34: rng <:q,an:> c= [:(rng q),(rng an):] by FUNCT_3:71;
dom (diffreal .: q,an) = dom (diffreal * <:q,an:>) by FUNCOP_1:def 3
.= dom <:q,an:> by A33, A34, RELAT_1:46, XBOOLE_1:1
.= (dom q) /\ (dom an) by FUNCT_3:def 8 ;
hence A35: dom q0 = (dom q) /\ (dom an) by RVSUM_1:def 6
.= (Seg m) /\ (Seg m) by A13, A24, FINSEQ_1:def 3
.= Seg m ;
:: thesis:

now

let j be Nat; :: thesis:
assume A36: j in dom q0 ; :: thesis:
consider s being FinSequence of REAL such that
A37: dom s = Seg (n + 1) and
A38: q . j = Sum s and
A39: for i being Nat st i in dom s holds
s . i = a . [i,j] by A13, A35, A36;
reconsider sn = s | (Seg n) as FinSequence of REAL by FINSEQ_1:23;
take sn = sn; :: thesis:
A40: len s = n + 1 by A37, FINSEQ_1:def 3;
then n <= len s by NAT_1:11;
hence A41: dom sn = Seg n by FINSEQ_1:21; :: thesis:
A42: sn ^ <*(s . (n + 1))*> = s by A40, FINSEQ_3:61;
s . (n + 1) = a . [(n + 1),j] by A37, A39, FINSEQ_1:6;
then s . (n + 1) = an . j by A24, A35, A36, A25;
then (q . j) - (an . j) = ((Sum sn) + (an . j)) - (an . j) by A38, A42, RVSUM_1:104
.= Sum sn ;
hence q0 . j = Sum sn by A36, VALUED_1:13; :: thesis:
thus for i being Nat st i in dom sn holds
sn . i = a0 . [i,j] :: thesis:

proof

let i be Nat; :: thesis:
assume A43: i in dom sn ; :: thesis:
A44: [i,j] in [:(Seg n),(Seg m):] by A35, A36, A41, A43, ZFMISC_1:106;
n <= n + 1 by NAT_1:11;
then A45: Seg n c= Seg (n + 1) by FINSEQ_1:7;
dom a = [:(Seg (n + 1)),(Seg m):] by FUNCT_2:def 1;
then A46: dom a0 = [:(Seg (n + 1)),(Seg m):] /\ [:(Seg n),(Seg m):] by FUNCT_1:68
.= [:(Seg n),(Seg m):] by A45, ZFMISC_1:124 ;
thus sn . i = s . i by A43, FUNCT_1:70
.= a . [i,j] by A37, A39, A41, A43, A45
.= a0 . [i,j] by A44, A46, FUNCT_1:70 ; :: thesis:

end;

hence for j being Nat st j in dom q0 holds
ex s being FinSequence of REAL st
( dom s = Seg n & q0 . j = Sum s & ( for i being Nat st i in dom s holds
s . i = a0 . [i,j] ) ) ; :: thesis:

end;

len p = n + 1 by A12, FINSEQ_1:def 3;
then A47: p0 ^ <*(Sum an)*> = p by A27, FINSEQ_3:61;
len q0 = m by A32, FINSEQ_1:def 3;
then A48: q0 is Element of m -tuples_on REAL by FINSEQ_2:110;
A49: an is Element of m -tuples_on REAL by A24, FINSEQ_2:110;
len q = m by A13, FINSEQ_1:def 3;
then q is Element of m -tuples_on REAL by FINSEQ_2:110;
then A50: q0 + an = q by A49, RVSUM_1:64;
thus Sum p = (Sum p0) + (Sum an) by A47, RVSUM_1:104
.= (Sum q0) + (Sum an) by A11, A14, A32
.= Sum q by A48, A49, A50, RVSUM_1:119 ; :: thesis:

end;

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

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A10); :: thesis: