let f be Function; :: thesis: ( rng f = {{}} implies product f = {} )
assume rng f = {{}} ; :: thesis: product f = {}
then {} in rng f by TARSKI:def 1;
hence product f = {} by CARD_3:26; :: thesis: verum