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

proof

set zeroseq = the Complex_Sequence;
the Complex_Sequence in Funcs (NAT,COMPLEX) 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 Complex_Sequence )
for x being set st x is Complex_Sequence holds
x in IT

proof

let x be set ; :: thesis: ( x is Complex_Sequence implies x in IT )
assume A2: x is Complex_Sequence ; :: thesis: x in IT
then x in Funcs (NAT,COMPLEX) 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 Complex_Sequence ) by A1; :: thesis: verum