reconsider F = <*(X --> 0)*> as FinSequence of Funcs (X,ExtREAL) by Th52;
take F ; :: thesis: F is summable
for n being Nat st n in dom F holds
F . n is without+infty by Th52;
hence F is summable by DEF10; :: thesis: verum