for i being natural Number
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