let k1, k2 be Nat; :: thesis: ( k1 <> k2 implies DataLoc (k1,0) <> DataLoc (k2,0) )
assume A1: k1 <> k2 ; :: thesis: DataLoc (k1,0) <> DataLoc (k2,0)
assume DataLoc (k1,0) = DataLoc (k2,0) ; :: thesis: contradiction
then |.(k1 + 0).| = |.(k2 + 0).| by XTUPLE_0:1;
then k1 = |.k2.| by ABSVALUE:def 1;
hence contradiction by A1, ABSVALUE:def 1; :: thesis: verum