theorem Th39: :: SF_MASTR:39

for i being Instruction of SCM+FSA
for k being Nat holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))