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 Element of 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 Element of 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 & ( for n being Nat st 0 <> n & n < len p holds
r . (n + 1) = (r . n) + (p . (n + 1)) ) & Sum p = r . (len p) ) by PROB_3:68;
deffunc H₁( Nat) -> Element of REAL = r . $1;
consider q being FinSequence such that
A3: ( len q = len p & ( for k being Nat st k in dom q holds
q . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A4: dom q = dom p by A3, FINSEQ_3:31;
A5: 1 in dom p by A1, FINSEQ_3:27;
rng q c= REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng q or x in REAL )
assume A6: x in rng q ; :: thesis: x in REAL
consider j being Nat such that
A7: ( j in dom q & q . j = x ) by A6, FINSEQ_2:11;
q . j = r . j by A3, A7;
hence x in REAL by A7; :: thesis: verum

end;

then reconsider q = q as FinSequence of REAL by FINSEQ_1:def 4;

A8: now

let k be Element of NAT ; :: thesis: ( 0 <> k & k < len p implies q . (k + 1) = (q . k) + (p . (k + 1)) )
assume A9: ( 0 <> k & k < len p ) ; :: thesis: q . (k + 1) = (q . k) + (p . (k + 1))
( k >= 1 & k <= len p & k + 1 >= 1 & k + 1 <= len p ) by A9, NAT_1:13, NAT_1:14;
then A10: ( k in dom q & k + 1 in dom q ) by A3, FINSEQ_3:27;
hence q . (k + 1) = r . (k + 1) by A3
.= (r . k) + (p . (k + 1)) by A2, A9
.= (q . k) + (p . (k + 1)) by A3, A10 ;
:: thesis: verum

end;

A11: len p in dom q by A3, A1, FINSEQ_3:27;
take q ; :: thesis: ( len q = len p & q . 1 = p . 1 & ( for k being Element of NAT st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) )
thus ( len q = len p & q . 1 = p . 1 & ( for k being Element of NAT st 0 <> k & k < len p holds
q . (k + 1) = (q . k) + (p . (k + 1)) ) & Sum p = q . (len p) ) by A2, A3, A5, A8, A11, A4; :: thesis: verum