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:11; :: thesis: verum