let i, j be Nat; :: 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 Th77;
then A: i |-> the Element of D in i -tuples_on D by Lemat;
assume i -tuples_on D = j -tuples_on A ; :: thesis: i = j
then i |-> the Element of D in j -tuples_on A by A;
then i |-> the Element of D is j -long by Lemat2;
then len (i |-> the Element of D) = j by FINSEQ_1:def 18;
hence i = j by FINSEQ_1:def 18; :: thesis: verum