defpred S_{1}[ 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 (MonMaps (S,T)) & S_{1}[a] ) )
from XBOOLE_0:sch 1();

X c= the carrier of (MonMaps (S,T)) by A1;

then reconsider X = X as Subset of (MonMaps (S,T)) ;

take SX = subrelstr X; :: thesis: for f being Function of S,T holds

( f in the carrier of SX iff f is continuous )

let f be Function of S,T; :: thesis: ( f in the carrier of SX iff f is continuous )

f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;

then f in the carrier of (MonMaps (S,T)) by A2, YELLOW_1:def 6;

then f in X by A1, A2;

hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum

( $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 (MonMaps (S,T)) & S

X c= the carrier of (MonMaps (S,T)) by A1;

then reconsider X = X as Subset of (MonMaps (S,T)) ;

take SX = subrelstr X; :: thesis: for f being Function of S,T holds

( f in the carrier of SX iff f is continuous )

let f be Function of S,T; :: thesis: ( f in the carrier of SX iff f is continuous )

hereby :: thesis: ( f is continuous implies f in the carrier of SX )

assume A2:
f is continuous
; :: thesis: f in the carrier of SXassume
f in the carrier of SX
; :: thesis: f is continuous

then f in X by YELLOW_0:def 15;

then ex f9 being Function of S,T st

( f9 = f & f9 is continuous ) by A1;

hence f is continuous ; :: thesis: verum

end;then f in X by YELLOW_0:def 15;

then ex f9 being Function of S,T st

( f9 = f & f9 is continuous ) by A1;

hence f is continuous ; :: thesis: verum

f in Funcs ( the carrier of S, the carrier of T) by FUNCT_2:8;

then f in the carrier of (MonMaps (S,T)) by A2, YELLOW_1:def 6;

then f in X by A1, A2;

hence f in the carrier of SX by YELLOW_0:def 15; :: thesis: verum