theorem Th25: :: SCMFSA9A:25

for b being Int-Location
for I being MacroInstruction of SCM+FSA holds UsedI*Loc (while>0 (b,I)) = UsedI*Loc I