for dl being Data-Location ex i being Nat st dl = dl. i