let x, y be set ; :: 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 A1: ( x in dom f & y in dom f & x <> y ) ; :: thesis: (disjoin f) . x misses (disjoin f) . y
consider z being Element of ((disjoin f) . x) /\ ((disjoin f) . y);
assume ((disjoin f) . x) /\ ((disjoin f) . y) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
then ( (disjoin f) . x = [:(f . x),{x}:] & (disjoin f) . y = [:(f . y),{y}:] & (disjoin f) . x = (disjoin f) . x & (disjoin f) . y = (disjoin f) . y & z in (disjoin f) . x & z in (disjoin f) . y ) by A1, Def3, XBOOLE_0:def 4;
then ( z `2 in {x} & z `2 in {y} ) by MCART_1:10;
then ( z `2 = x & z `2 = y ) by TARSKI:def 1;
hence contradiction by A1; :: thesis: verum