( 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