theorem Th4: :: SCMPDS_4:4

for dl being Int_position ex i being Nat st dl = DataLoc (i,0)