set s1 = seq_const 1;
set S = NAT --> (seq_const 1);
A1: dom (NAT --> (seq_const 1)) = NAT by FUNCOP_1:13;
A2: Funcs (NAT,REAL) c= PFuncs (NAT,REAL) by FUNCT_2:72;
seq_const 1 in Funcs (NAT,REAL) by FUNCT_2:8;
then A3: seq_const 1 in PFuncs (NAT,REAL) by A2;
PFuncs (NAT,REAL) c= PFuncs (REAL,REAL) by NUMBERS:19, PARTFUN1:50;
then A4: seq_const 1 in PFuncs (REAL,REAL) by A3;
A5: {(seq_const 1)} c= PFuncs (REAL,REAL) by A4, ZFMISC_1:31;
rng (NAT --> (seq_const 1)) c= PFuncs (REAL,REAL) by A5, XBOOLE_1:1;
then reconsider S = NAT --> (seq_const 1) as Functional_Sequence of REAL,REAL by A1, FUNCT_2:2;
take S ; :: thesis: for n being Nat holds S . n is Real_Sequence
let n be Nat; :: thesis: S . n is Real_Sequence
n in NAT by ORDINAL1:def 12;
then S . n = seq_const 1 by FUNCOP_1:7;
hence S . n is Real_Sequence ; :: thesis: verum