reconsider F = <*> ExtREAL as FinSequence of ExtREAL ;
ex f being Function of NAT ,ExtREAL st
( Sum F = f . (len F) & f . 0 = 0. & ( for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) ) by Def5;
hence Sum (<*> ExtREAL ) = 0. ; :: thesis: verum