reconsider mm = m as Element of NAT by ORDINAL1:def 12;
mm -tuples_on X c= X * by FINSEQ_2:134;
hence for b₁ being set st b₁ = (m -tuples_on X) \ (X *) holds
b₁ is empty ; :: thesis: verum