let m be non zero Nat; :: thesis: for s being FinSequence of REAL m
for j being Nat st 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
defpred S₁[ Nat] means for s being FinSequence of REAL m
for j being Nat st len s = $1 & 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t );
A1: S₁[ 0 ]

proof

let s be FinSequence of REAL m; :: thesis: for j being Nat st len s = 0 & 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
let j be Nat; :: thesis: ( len s = 0 & 1 <= j & j <= m implies ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t ) )
assume A2: ( len s = 0 & 1 <= j & j <= m ) ; :: thesis: ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
reconsider t = <*> REAL as FinSequence of REAL ;
take t ; :: thesis: ( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
thus len t = len s by A2; :: thesis: ( ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
thus for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) by A2; :: thesis: (Sum s) . j = Sum t
(Sum s) . j = (0* m) . j by EUCLID_7:def 11, A2
.= 0 ;
hence (Sum s) . j = Sum t by RVSUM_1:72; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let s be FinSequence of REAL m; :: thesis: for j being Nat st len s = n + 1 & 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
let j be Nat; :: thesis: ( len s = n + 1 & 1 <= j & j <= m implies ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t ) )
reconsider sn = s | n as FinSequence of REAL m ;
assume A5: ( len s = n + 1 & 1 <= j & j <= m ) ; :: thesis: ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
then A6: len sn = n by FINSEQ_1:59, NAT_1:11;
A7: s = sn ^ <*(s . (n + 1))*> by A5, FINSEQ_3:55;
n + 1 in Seg (n + 1) by FINSEQ_1:4;
then n + 1 in dom s by A5, FINSEQ_1:def 3;
then s . (n + 1) in rng s by FUNCT_1:3;
then reconsider sn1 = s . (n + 1) as Element of REAL m ;
A8: Sum s = (Sum sn) + sn1 by Th3, A7;
len (Sum sn) = m by CARD_1:def 7;
then dom (Sum sn) = Seg m by FINSEQ_1:def 3;
then j in dom (Sum sn) by A5;
then A9: (Sum sn) . j in rng (Sum sn) by FUNCT_1:3;
len sn1 = m by CARD_1:def 7;
then dom sn1 = Seg m by FINSEQ_1:def 3;
then j in dom sn1 by A5;
then sn1 . j in rng sn1 by FUNCT_1:3;
then reconsider x = (Sum sn) . j, y = sn1 . j as Element of REAL by A9;
A10: (Sum s) . j = x + y by A8, RVSUM_1:11;
consider tn being FinSequence of REAL such that
A11: ( len tn = len sn & ( for i being Nat st 1 <= i & i <= len sn holds
ex sni being Element of REAL m st
( sni = sn . i & tn . i = sni . j ) ) & (Sum sn) . j = Sum tn ) by A4, A5, A6;
reconsider t = tn ^ <*y*> as FinSequence of REAL ;
take t ; :: thesis: ( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
thus len t = (len tn) + (len <*y*>) by FINSEQ_1:22
.= n + (len <*y*>) by A5, A11, FINSEQ_1:59, NAT_1:11
.= len s by A5, FINSEQ_1:40 ; :: thesis: ( ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t )
thus for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) :: thesis: (Sum s) . j = Sum t

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len s implies ex si being Element of REAL m st
( si = s . i & t . i = si . j ) )
assume A12: ( 1 <= i & i <= len s ) ; :: thesis: ex si being Element of REAL m st
( si = s . i & t . i = si . j )

per cases ( i <> len s or i = len s ) ;

suppose i <> len s ; :: thesis: ex si being Element of REAL m st
( si = s . i & t . i = si . j )

then i < n + 1 by A5, A12, XXREAL_0:1;
then A13: i <= n by NAT_1:13;
then consider sni being Element of REAL m such that
A14: ( sni = sn . i & tn . i = sni . j ) by A6, A11, A12;
take sni ; :: thesis: ( sni = s . i & t . i = sni . j )
i in Seg n by A12, A13;
hence sni = s . i by A14, FUNCT_1:49; :: thesis: t . i = sni . j
i in Seg (len tn) by A6, A11, A12, A13;
then i in dom tn by FINSEQ_1:def 3;
hence t . i = sni . j by A14, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A15: i = len s ; :: thesis: ex si being Element of REAL m st
( si = s . i & t . i = si . j )

take sn1 ; :: thesis: ( sn1 = s . i & t . i = sn1 . j )
thus sn1 = s . i by A5, A15; :: thesis: t . i = sn1 . j
thus t . i = sn1 . j by A5, A6, A11, A15, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

thus (Sum s) . j = Sum t by RVSUM_1:74, A11, A10; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
hence for s being FinSequence of REAL m
for j being Nat st 1 <= j & j <= m holds
ex t being FinSequence of REAL st
( len t = len s & ( for i being Nat st 1 <= i & i <= len s holds
ex si being Element of REAL m st
( si = s . i & t . i = si . j ) ) & (Sum s) . j = Sum t ) ; :: thesis: verum