let F be Cardinal-Function; :: thesis: for x being set st x in dom F holds
card ((disjoin F) . x) = F . x
let x be set ; :: 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 & M,[:M,{x}:] are_equipotent & M = card M ) by CARD_1:def 5, CARD_2:13;
then ( M = card [:M,{x}:] & (disjoin F) . x = [:M,{x}:] ) by A1, Def3, CARD_1:21;
hence card ((disjoin F) . x) = F . x ; :: thesis: verum