for D being non empty set
for m, n being Nat holds
( [:(n -tuples_on D),(m -tuples_on D):],(n + m) -tuples_on D are_equipotent & card [:(n -tuples_on D),(m -tuples_on D):] = card ((n + m) -tuples_on D) )