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