theorem :: CARD_3:31

for F being Cardinal-Function holds
( {} in rng F iff Product F = 0 )