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:33;
then k1 = abs k2 by ABSVALUE:def 1;
hence contradiction by A1, ABSVALUE:def 1; :: thesis: verum