theorem Th29: :: CARD_3:29

for F being Cardinal-Function
for x being object st x in dom F holds
card ((disjoin F) . x) = F . x