let F be Cardinal-Function; :: thesis: for x being object st x in dom F holds
card ((disjoin F) . x) = F . x
let x be object ; :: thesis: ( x in dom F implies card ((disjoin F) . x) = F . x )
assume A1: x in dom F ; :: thesis: card ((disjoin F) . x) = F . x
then reconsider M = F . x as Cardinal by Def1;
M,[:M,{x}:] are_equipotent by CARD_1:69;
then M = card [:M,{x}:] by CARD_1:def 2;
hence card ((disjoin F) . x) = F . x by A1, Def3; :: thesis: verum