ex f being Function st
( F . n = f & dom f = NAT & rng f c= PFuncs (X,ExtREAL) ) by FUNCT_2:def 2;
hence F . n is Functional_Sequence of X,ExtREAL by FUNCT_2:def 1, RELSET_1:4; :: thesis: verum