let a be FinSequence of REAL ; :: thesis: ex s being XFinSequence of REAL st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) )
deffunc H1( Nat) -> object = Sum (a | $1);
ex p being XFinSequence st
( len p = (len a) + 1 & ( for k being Nat st k in (len a) + 1 holds
p . k = H1(k) ) ) from AFINSQ_1:sch 2();
 then consider p being XFinSequence such that
A1: len p = (len a) + 1 and
A2: for k being Nat st k in (len a) + 1 holds
p . k = H1(k) ;
rng p c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in REAL )
assume y in rng p ; :: thesis: y in REAL
then consider x being object such that
A3: x in dom p and
A4: y = p . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A3;
p . nx = Sum (a | nx) by A1, A2, A3;
hence y in REAL by A4, XREAL_0:def 1; :: thesis: verum
end;
then reconsider p = p as XFinSequence of REAL by RELAT_1:def 19;
A5: for i being Nat st i < len a holds
p . (i + 1) = (p . i) + (a . (i + 1))
proof
let i be Nat; :: thesis: ( i < len a implies p . (i + 1) = (p . i) + (a . (i + 1)) )
assume A6: i < len a ; :: thesis: p . (i + 1) = (p . i) + (a . (i + 1))
reconsider i = i as Element of NAT by ORDINAL1:def 12;
reconsider ii = i + 1 as Nat ;
A7: i + 1 <= len a by A6, NAT_1:13;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg (len a) by A7, FINSEQ_1:1;
then A8: i + 1 in dom a by FINSEQ_1:def 3;
i < (len a) + 1 by A6, NAT_1:13;
then i in Segm ((len a) + 1) by NAT_1:44;
then A9: p . i = Sum (a | i) by A2;
i + 1 < (len a) + 1 by A6, XREAL_1:6;
then A10: i + 1 in Segm ((len a) + 1) by NAT_1:44;
a | ii = (a | i) ^ <*(a /. ii)*> by A7, FINSEQ_5:82;
then Sum (a | ii) = (Sum (a | i)) + (Sum <*(a /. ii)*>) by RVSUM_1:75
.= (p . i) + (a /. ii) by A9, RVSUM_1:73
.= (p . i) + (a . ii) by A8, PARTFUN1:def 6 ;
hence p . (i + 1) = (p . i) + (a . (i + 1)) by A2, A10; :: thesis: verum
end;
0 in Segm ((len a) + 1) by NAT_1:44;
then A11: p . 0 = H1( 0 ) by A2
.= 0 by RVSUM_1:72 ;
then Sum a = p . (len a) by A5, Th3;
hence ex s being XFinSequence of REAL st
( len s = (len a) + 1 & s . 0 = 0 & ( for i being Nat st i < len a holds
s . (i + 1) = (s . i) + (a . (i + 1)) ) & Sum a = s . (len a) ) by A1, A11, A5; :: thesis: verum