let x, y be object ; :: thesis: for f being Function st x in dom f & y in dom f & x <> y holds
(disjoin f) . x misses (disjoin f) . y
let f be Function; :: thesis: ( x in dom f & y in dom f & x <> y implies (disjoin f) . x misses (disjoin f) . y )
assume that
A1: x in dom f and
A2: y in dom f and
A3: x <> y ; :: thesis: (disjoin f) . x misses (disjoin f) . y
set z = the Element of ((disjoin f) . x) /\ ((disjoin f) . y);
assume A4: ((disjoin f) . x) /\ ((disjoin f) . y) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
A5: (disjoin f) . x = [:(f . x),{x}:] by A1, Def3;
A6: (disjoin f) . y = [:(f . y),{y}:] by A2, Def3;
A7: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) in (disjoin f) . x by A4, XBOOLE_0:def 4;
A8: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) in (disjoin f) . y by A4, XBOOLE_0:def 4;
A9: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 in {x} by A5, A7, MCART_1:10;
A10: the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 in {y} by A6, A8, MCART_1:10;
the Element of ((disjoin f) . x) /\ ((disjoin f) . y) `2 = x by A9, TARSKI:def 1;
hence contradiction by A3, A10, TARSKI:def 1; :: thesis: verum