let A1, A2 be strict full SubRelStr of MonMaps S,T; :: thesis: ( ( for f being Function of S,T holds
( f in the carrier of A1 iff f is continuous ) ) & ( for f being Function of S,T holds
( f in the carrier of A2 iff f is continuous ) ) implies A1 = A2 )
assume that
A5: for f being Function of S,T holds
( f in the carrier of A1 iff f is continuous ) and
A6: for f being Function of S,T holds
( f in the carrier of A2 iff f is continuous ) ; :: thesis: A1 = A2
A7: the carrier of A1 c= the carrier of (MonMaps S,T) by YELLOW_0:def 13;
A8: the carrier of A2 c= the carrier of (MonMaps S,T) by YELLOW_0:def 13;
the carrier of A1 = the carrier of A2

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of A2 c= the carrier of A1

let x be set ; :: thesis: ( x in the carrier of A1 implies x in the carrier of A2 )
assume A9: x in the carrier of A1 ; :: thesis: x in the carrier of A2
then reconsider y = x as Element of A1 ;
reconsider y = y as Function of S,T by A7, A9, WAYBEL10:10;
y is continuous by A5, A9;
hence x in the carrier of A2 by A6; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A2 or x in the carrier of A1 )
assume A10: x in the carrier of A2 ; :: thesis: x in the carrier of A1
then reconsider y = x as Element of A2 ;
reconsider y = y as Function of S,T by A8, A10, WAYBEL10:10;
y is continuous by A6, A10;
hence x in the carrier of A1 by A5; :: thesis: verum

end;

hence A1 = A2 by YELLOW_0:58; :: thesis: verum