let p be FinSequence of REAL ; ( 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
; 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 H1( 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 = H1(k) ) )
from FINSEQ_1:sch 2();
A7:
rng q c= REAL
A10:
dom q = dom p
by A6, FINSEQ_3:29;
reconsider q = q as FinSequence of REAL by A7, FINSEQ_1:def 4;
take
q
; ( 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; verum