defpred S₁[ set ] means $1 is Real_Sequence;
consider IT being set such that
A1: for x being set holds
( x in IT iff ( x in Funcs (NAT,REAL) & S₁[x] ) ) from XBOOLE_0:sch 1();
not IT is empty

proof

set zeroseq = the Real_Sequence;
the Real_Sequence in Funcs (NAT,REAL) by FUNCT_2:8;
hence not IT is empty by A1; :: thesis: verum

end;

then reconsider IT = IT as non empty set ;
take IT ; :: thesis: for x being set holds
( x in IT iff x is Real_Sequence )
for x being set st x is Real_Sequence holds
x in IT

proof

let x be set ; :: thesis: ( x is Real_Sequence implies x in IT )
assume A2: x is Real_Sequence ; :: thesis: x in IT
then x in Funcs (NAT,REAL) by FUNCT_2:8;
hence x in IT by A1, A2; :: thesis: verum

end;

hence for x being set holds
( x in IT iff x is Real_Sequence ) by A1; :: thesis: verum