consider S being Functional_Sequence of REAL,REAL such that
A1: for n being Element of NAT holds S . n is Real_Sequence by Lm1;
take S ; :: thesis: S is Sequence-yielding
thus S is Sequence-yielding by A1, Def12; :: thesis: verum