consider S being Functional_Sequence of REAL ,REAL ;
consider s1 being Real_Sequence;
set s1 = NAT --> 1;
A1: dom (NAT --> 1) = NAT by FUNCOP_1:19;
for n being Element of NAT holds (NAT --> 1) . n is real ;
then A2: NAT --> 1 is Real_Sequence by A1, SEQ_1:4;
A4: NAT --> 1 is PartFunc of REAL ,REAL by RELSET_1:17;
set S = NAT --> (NAT --> 1);
A5: dom (NAT --> (NAT --> 1)) = NAT by FUNCOP_1:19;
for n being Element of NAT holds (NAT --> (NAT --> 1)) . n is PartFunc of REAL ,REAL by A4, FUNCOP_1:13;
then reconsider S = NAT --> (NAT --> 1) as Functional_Sequence of REAL ,REAL by A5, SEQFUNC:1;
for n being Element of NAT holds S . n is Real_Sequence by A2, FUNCOP_1:13;
hence ex S being Functional_Sequence of REAL ,REAL st
for n being Element of NAT holds S . n is Real_Sequence ; :: thesis: verum