let p be FinSequence of REAL ; :: thesis: ( len p >= 1 implies ex q being FinSequence of REAL st
( len q = len p & q . 1 = p . 1 & ( for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) ) )
assume A1: len p >= 1 ; :: thesis: ex q being FinSequence of REAL st
( len q = len p & q . 1 = p . 1 & ( for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) )
then consider r being Real_Sequence such that
A2: r . 1 = p . 1 and
A3: for n being Nat st 0 <> n & n < len p holds
r . (n + 1) = (r . n) + (p . (n + 1)) and
A4: Sum p = r . (len p) by PROB_3:63;
A5: 1 in dom p by A1, FINSEQ_3:25;
deffunc H₁( Nat) -> set = r . $1;
consider q being FinSequence such that
A6: ( len q = len p & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A7: rng q c= REAL

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in REAL )
assume x in rng q ; :: thesis: x in REAL
then consider j being Nat such that
A8: j in dom q and
A9: q . j = x by FINSEQ_2:10;
H₁(j) = q . j by A6, A8;
hence x in REAL by A9, XREAL_0:def 1; :: thesis: verum

end;

A10: dom q = dom p by A6, FINSEQ_3:29;
reconsider q = q as FinSequence of REAL by A7, FINSEQ_1:def 4;

A11: now :: thesis: for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1))

let k be Nat; :: thesis: ( 0 <> k & k < len p implies q . (k + 1) = (q . k) + (p . (k + 1)) )
assume that
A12: 0 <> k and
A13: k < len p ; :: thesis: q . (k + 1) = (q . k) + (p . (k + 1))
k >= 1 by A12, NAT_1:14;
then A14: k in dom q by A6, A13, FINSEQ_3:25;
A15: k + 1 >= 1 by NAT_1:14;
k + 1 <= len p by A13, NAT_1:13;
then k + 1 in dom q by A6, A15, FINSEQ_3:25;
hence q . (k + 1) = r . (k + 1) by A6
.= (r . k) + (p . (k + 1)) by A3, A12, A13
.= (q . k) + (p . (k + 1)) by A6, A14 ;
:: thesis: verum

end;

take q ; :: thesis: ( len q = len p & q . 1 = p . 1 & ( for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) )
len p in dom q by A1, A6, FINSEQ_3:25;
hence ( len q = len p & q . 1 = p . 1 & ( for k being Nat st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) ) by A2, A4, A6, A10, A5, A11; :: thesis: verum