A: dom f = NAT by SEQFUNC:1;
for n being Element of NAT holds f . n is PartFunc of X,ExtREAL by NUMBERS:31, RELSET_1:17;
hence f is Functional_Sequence of X,ExtREAL by A, SEQFUNC:1; :: thesis: verum