let i, j be natural Number ; :: thesis: for A being set
for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
let A be set ; :: thesis: for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
let D be non empty set ; :: thesis: ( i -tuples_on D = j -tuples_on A implies i = j )
set f = i |-> the Element of D;
i |-> the Element of D is Tuple of i,D by Th61;
then A1: i |-> the Element of D in i -tuples_on D by Lm6;
assume i -tuples_on D = j -tuples_on A ; :: thesis: i = j
then i |-> the Element of D in j -tuples_on A by A1;
then i |-> the Element of D is j -element by Lm7;
then len (i |-> the Element of D) = j ;
hence i = j by CARD_1:def 7; :: thesis: verum