{} in {{}} by TARSKI:def 1;
then {} in rng <*{}*> by FINSEQ_1:39;
hence product <*{}*> is empty by CARD_3:26; :: thesis: verum