defpred S₁[ object ] means ex f being Function of S,T st
( $1 = f & f is continuous );
consider X being set such that
A1: for a being object 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) by A1;
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 f9 being Function of S,T st
( f9 = f & f9 is continuous )
then f in X by YELLOW_0:def 15;
then consider f9 being Function of S,T such that
A2: ( f9 = f & f9 is continuous ) by A1;
take f9 = f9; :: thesis: ( f9 = f & f9 is continuous )
thus ( f9 = f & f9 is continuous ) by A2; :: thesis: verum

end;

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