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 H_{1}( 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 = H_{1}(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 = H_{1}(k)
;

rng p c= REAL

A5: for i being Nat st i < len a holds

p . (i + 1) = (p . i) + (a . (i + 1))

then A11: p . 0 = H_{1}( 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

( 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 H

ex p being XFinSequence st

( len p = (len a) + 1 & ( for k being Nat st k in (len a) + 1 holds

p . k = H

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 = H

rng p c= REAL

proof

then reconsider p = p as XFinSequence of REAL by RELAT_1:def 19;
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;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

A5: for i being Nat st i < len a holds

p . (i + 1) = (p . i) + (a . (i + 1))

proof

0 in Segm ((len a) + 1)
by NAT_1:44;
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;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

then A11: p . 0 = H

.= 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