ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & Sum f = g . ((len f) -' 1) ) by Def4;
hence Sum f = 0 by FUNCT_1:def 4; :: according to XXREAL_0:def 8 :: thesis: verum