( dom f = NAT & ( for n being Nat holds f . n is PartFunc of X,ExtREAL ) )
by NUMBERS:31, RELSET_1:7, SEQFUNC:1;

hence f is Functional_Sequence of X,ExtREAL by SEQFUNC:1; :: thesis: verum

hence f is Functional_Sequence of X,ExtREAL by SEQFUNC:1; :: thesis: verum