let k1, k2 be Element of 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 abs (k1 + 0) = abs (k2 + 0) by ZFMISC_1:27;
then k1 = abs k2 by ABSVALUE:def 1;
hence contradiction by A1, ABSVALUE:def 1; :: thesis: verum