theorem Th1: :: AMI_5:1

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