theorem :: AMI_5:16

for s being State of SCM
for iloc being Nat
for a being Data-Location holds s . a = (s +* (Start-At (iloc,SCM))) . a