let F be Cardinal-Function; :: thesis: ( {} in rng F iff Product F = 0 )
thus ( {} in rng F implies Product F = 0 ) by Th37, CARD_1:47; :: thesis: ( Product F = 0 implies {} in rng F )
assume Product F = 0 ; :: thesis: {} in rng F
then product F, {} are_equipotent ;
then product F = {} by CARD_1:46;
hence {} in rng F by Th37; :: thesis: verum