theorem Th24: :: SF_MASTR:24

for p being preProgram of SCM+FSA
for k being Nat holds UsedILoc p = UsedILoc (IncAddr (p,k))