consider s1 being Real_Sequence;
consider S being Functional_Sequence of REAL ,REAL ;
set s1 = NAT --> 1;
set S = NAT --> (NAT --> 1);
NAT --> 1 is PartFunc of REAL ,REAL by RELSET_1:17;
then ( dom (NAT --> (NAT --> 1)) = NAT & ( for n being Element of NAT holds (NAT --> (NAT --> 1)) . n is PartFunc of REAL ,REAL ) ) by FUNCOP_1:13, FUNCOP_1:19;
then reconsider S = NAT --> (NAT --> 1) as Functional_Sequence of REAL ,REAL by SEQFUNC:1;
( dom (NAT --> 1) = NAT & ( for n being Element of NAT holds (NAT --> 1) . n is real ) ) by FUNCOP_1:19;
then NAT --> 1 is Real_Sequence by SEQ_1:4;
then for n being Element of NAT holds S . n is Real_Sequence by 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