let i, j be Nat; :: thesis: for D being non empty set st i -tuples_on D = j -tuples_on D holds
i = j
let D be non empty set ; :: thesis: ( i -tuples_on D = j -tuples_on D implies i = j )
consider d being Element of D;
( i |-> d is FinSequence of D & len (i |-> d) = i ) by FINSEQ_1:def 18, Th77;
then reconsider id1 = i |-> d as Element of i -tuples_on D by Th110;
assume i -tuples_on D = j -tuples_on D ; :: thesis: i = j
then ( len id1 = i & len id1 = j ) by FINSEQ_1:def 18;
hence i = j ; :: thesis: verum