let D1, D2 be non empty set ; :: thesis: for n, m being Nat st n -tuples_on D1 = m -tuples_on D2 holds
n = m
let n, m be Nat; :: thesis: ( n -tuples_on D1 = m -tuples_on D2 implies n = m )
assume A1: n -tuples_on D1 = m -tuples_on D2 ; :: thesis: n = m
consider p being Element of n -tuples_on D1;
p in m -tuples_on D2 by A1;
then consider w being Element of D2 * such that
A2: ( p = w & len w = m ) ;
thus n = m by A2, FINSEQ_1:def 18; :: thesis: verum