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
A3: for f being Function of S,T holds
( f in the carrier of A1 iff f is continuous ) and
A4: for f being Function of S,T holds
( f in the carrier of A2 iff f is continuous ) ; :: thesis: A1 = A2
A5: the carrier of A1 c= the carrier of (MonMaps (S,T)) by YELLOW_0:def 13;
A6: 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 object ; :: thesis: ( x in the carrier of A1 implies x in the carrier of A2 )
assume A7: 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 A5, A7, WAYBEL10:9;
y is continuous by A3, A7;
hence x in the carrier of A2 by A4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A2 or x in the carrier of A1 )
assume A8: 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 A6, A8, WAYBEL10:9;
y is continuous by A4, A8;
hence x in the carrier of A1 by A3; :: thesis: verum
end;
hence A1 = A2 by YELLOW_0:57; :: thesis: verum