not len {} = m1 ;
then {} is not Element of m1 -tuples_on U by CARD_1:def 7;
hence m1 -tuples_on U is with_non-empty_elements by SETFAM_1:def 8; :: thesis: verum