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