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