theorem :: SCMFSA_2:8

for dl being Int-Location ex i being Nat st dl = intloc i