let i be natural Number ; :: thesis: for D being non empty set
for z1, z2 being Tuple of i,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 Tuple of i,D st ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) holds
z1 = z2
let z1, z2 be Tuple of i,D; :: thesis: ( ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) implies z1 = z2 )
len z2 = i by CARD_1:def 7;
then A1: dom z2 = Seg i by FINSEQ_1:def 3;
len z1 = i by CARD_1:def 7;
then dom z1 = 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 A1; :: thesis: verum