reconsider z = 0 as Element of ExtREAL by XXREAL_0:def 1;
reconsider M = NAT --> z as ExtREAL_sequence ;
reconsider M = M as V184() ExtREAL_sequence by Lm2;
take M ; :: thesis: M is convergent
for n being Nat holds M . n = 0 by Lm1;
then M is convergent_to_finite_number by MESFUNC5:52;
hence M is convergent ; :: thesis: verum