let i be Nat; :: thesis: for D being non empty set
for z1, z2 being Element of i -tuples_on D st ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) holds
z1 = z2
let D be non empty set ; :: thesis: for z1, z2 being Element of i -tuples_on D st ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) holds
z1 = z2
let z1, z2 be Element of i -tuples_on D; :: thesis: ( ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) implies z1 = z2 )
( len z1 = i & len z2 = i ) by FINSEQ_1:def 18;
then ( dom z1 = Seg i & dom z2 = Seg i ) by FINSEQ_1:def 3;
hence ( ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) implies z1 = z2 ) by FINSEQ_1:17; :: thesis: verum