let Y be set ; :: thesis: for m being Nat holds (m + 1) -tuples_on Y c= (Y *) \ {{}}
let m be Nat; :: thesis: (m + 1) -tuples_on Y c= (Y *) \ {{}}
reconsider k = m, K = m + 1 as Element of NAT by ORDINAL1:def 12;
A1: 0 -tuples_on Y misses K -tuples_on Y by Lm5;
K -tuples_on Y c= (Y *) \ (0 -tuples_on Y) by FINSEQ_2:134, XBOOLE_1:86, A1;
hence (m + 1) -tuples_on Y c= (Y *) \ {{}} by Lm6; :: thesis: verum