now :: thesis: for x being object st x in dom (disjoin f) holds
(disjoin f) . x is empty

let x be object ; :: thesis: ( x in dom (disjoin f) implies (disjoin f) . x is empty )
assume x in dom (disjoin f) ; :: thesis: (disjoin f) . x is empty
then A1: x in dom f by CARD_3:def 3;
[:(f . x),{x}:] is empty ;
hence (disjoin f) . x is empty by A1, CARD_3:def 3; :: thesis: verum

end;

hence disjoin f is empty-yielding by FUNCT_1:def 8; :: thesis: verum