:: deftheorem defines Sum CARD_3:def 7 :
for F being Cardinal-Function holds Sum F = card (Union (disjoin F));