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

end;

assume A9: ( 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 (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 by A1, XBOOLE_0:def 4;
A12: z in X by A2, A10, XBOOLE_0:def 4;
then (X --> x) . z = x by FUNCOP_1:13;
hence (X --> x) . z = (Y --> y) . z by A9, A12, A11, FUNCOP_1:13, XBOOLE_0:3; :: thesis: verum