theorem Th35: :: SF_MASTR:35

for i being Instruction of SCM+FSA
for p being preProgram of SCM+FSA st i in rng p holds
UsedInt*Loc i c= UsedI*Loc p by Lm4;