:: deftheorem Def3 defines disjoin CARD_3:def 3 :
for f, b₂ being Function holds
( b₂ = disjoin f iff ( dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = [:(f . x),{x}:] ) ) );