let X, Y, x, y be set ; :: thesis: ( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )
set f = X --> x;
set g = Y --> y;
A1: ( dom (X --> x) = X & dom (Y --> y) = Y ) by FUNCOP_1:19;
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
A2: for z being set st z in (dom (X --> x)) /\ (dom (Y --> y)) holds
(X --> x) . z = (Y --> y) . z and
A3: x <> y ; :: according to PARTFUN1:def 6 :: thesis: X misses Y
assume X meets Y ; :: thesis: contradiction
then consider z being set such that
A4: ( z in X & z in Y ) by XBOOLE_0:3;
( z in X /\ Y & (X --> x) . z = x & (Y --> y) . z = y ) by A4, FUNCOP_1:13, XBOOLE_0:def 4;
hence contradiction by A1, A2, A3; :: thesis: verum

end;

assume A5: ( x = y or X misses Y ) ; :: thesis: X --> x tolerates Y --> y
let z be set ; :: according to PARTFUN1:def 6 :: thesis: ( not z in (dom (X --> x)) /\ (dom (Y --> y)) or (X --> x) . z = (Y --> y) . z )
assume z in (dom (X --> x)) /\ (dom (Y --> y)) ; :: thesis: (X --> x) . z = (Y --> y) . z
then ( z in X & z in Y ) by A1, XBOOLE_0:def 4;
then ( (X --> x) . z = x & (Y --> y) . z = y & x = y ) by A5, FUNCOP_1:13, XBOOLE_0:3;
hence (X --> x) . z = (Y --> y) . z ; :: thesis: verum