theorem Th22: :: SF_MASTR:22

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