set s1 = NAT --> 1;
set S = NAT --> (NAT --> 1);
NAT --> 1 is PartFunc of REAL,REAL by RELSET_1:7;
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:7, FUNCOP_1:13;
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:13;
then NAT --> 1 is Real_Sequence by SEQ_1:2;
then for n being Element of NAT holds S . n is Real_Sequence by FUNCOP_1:7;
hence ex S being Functional_Sequence of REAL,REAL st
for n being Element of NAT holds S . n is Real_Sequence ; :: thesis: verum