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

( 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

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: verumhereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: the carrier of A2 c= the carrier of A1

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of A2 or x in 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;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

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