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 )

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

( 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 A9:
( x = y or X misses Y )
; :: thesis: X --> x tolerates Y --> y
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;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

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