defpred S₁[ set ] means ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set such that
A1: for a being set holds
( a in X iff ( a in the carrier of (T |^ the carrier of S) & S₁[a] ) ) from XBOOLE_0:sch 1();
X c= the carrier of (T |^ the carrier of S)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in the carrier of (T |^ the carrier of S) )
assume a in X ; :: thesis: a in the carrier of (T |^ the carrier of S)
hence a in the carrier of (T |^ the carrier of S) by A1; :: thesis: verum

end;

then reconsider X = X as Subset of (T |^ the carrier of S) ;
take SX = subrelstr X; :: thesis: ( SX is full SubRelStr of T |^ the carrier of S & ( for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) ) ) )
thus SX is full SubRelStr of T |^ the carrier of S ; :: thesis: for x being set holds
( x in the carrier of SX iff ex f being Function of S,T st
( x = f & f is continuous ) )
let f be set ; :: thesis: ( f in the carrier of SX iff ex f being Function of S,T st
( f = f & f is continuous ) )

hereby :: thesis: ( ex f being Function of S,T st
( f = f & f is continuous ) implies f in the carrier of SX )

assume f in the carrier of SX ; :: thesis: ex f' being Function of S,T st
( f' = f & f' is continuous )
then f in X by YELLOW_0:def 15;
then consider f' being Function of S,T such that
A2: ( f' = f & f' is continuous ) by A1;
take f' = f'; :: thesis: ( f' = f & f' is continuous )
thus ( f' = f & f' is continuous ) by A2; :: thesis: verum

end;

given f' being Function of S,T such that A3: ( f = f' & f' is continuous ) ; :: thesis: f in the carrier of SX
f in Funcs the carrier of S,the carrier of T by A3, FUNCT_2:11;
then f in the carrier of (T |^ the carrier of S) by YELLOW_1:28;
then f in X by A1, A3;
hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum