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

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