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 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:
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 ; :: 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 ;
1 <= 1 + i by NAT_1:11;
then i + 1 in Seg (len a) by ;
then A8: i + 1 in dom a by FINSEQ_1:def 3;
i < (len a) + 1 by ;
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 ;
then A10: i + 1 in Segm ((len a) + 1) by NAT_1:44;
a | ii = (a | i) ^ <*(a /. ii)*> by ;
then Sum (a | ii) = (Sum (a | i)) + (Sum <*(a /. ii)*>) by RVSUM_1:75
.= (p . i) + (a /. ii) by
.= (p . i) + (a . ii) by ;
hence p . (i + 1) = (p . i) + (a . (i + 1)) by ; :: 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 ;
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