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