theorem Th1: :: SCMP_GCD:1

for n1, n2 being Nat holds DataLoc (n1,n2) = intpos (n1 + n2)