let X, Y be set ; :: thesis: for x, y being object holds
( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )
let x, y be object ; :: thesis: ( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )
set f = X --> x;
set g = Y --> y;
thus ( not X --> x tolerates Y --> y or x = y or X misses Y ) :: thesis: ( ( x = y or X misses Y ) implies X --> x tolerates Y --> y )

proof

assume that
A3: for z being object st z in (dom (X --> x)) /\ (dom (Y --> y)) holds
(X --> x) . z = (Y --> y) . z and
A4: x <> y ; :: according to PARTFUN1:def 4 :: thesis: X misses Y
assume X meets Y ; :: thesis: contradiction
then consider z being object such that
A5: z in X and
A6: z in Y by XBOOLE_0:3;
A7: (X --> x) . z = x by A5, Th7;
A8: (Y --> y) . z = y by A6, Th7;
z in X /\ Y by A5, A6, XBOOLE_0:def 4;
hence contradiction by A3, A4, A7, A8; :: thesis: verum

end;

assume A9: ( x = y or X misses Y ) ; :: thesis: X --> x tolerates Y --> y
let z be object ; :: according to PARTFUN1:def 4 :: thesis: ( not z in (proj1 (X --> x)) /\ (proj1 (Y --> y)) or (X --> x) . z = (Y --> y) . z )
assume A10: z in (dom (X --> x)) /\ (dom (Y --> y)) ; :: thesis: (X --> x) . z = (Y --> y) . z
then A11: z in Y ;
A12: z in X by A10, XBOOLE_0:def 4;
then (X --> x) . z = x by Th7;
hence (X --> x) . z = (Y --> y) . z by A9, A12, A11, Th7, XBOOLE_0:3; :: thesis: verum