let b be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds UsedI*Loc (Times (b,I)) = UsedI*Loc I
let I be MacroInstruction of SCM+FSA ; :: thesis: UsedI*Loc (Times (b,I)) = UsedI*Loc I
thus UsedI*Loc (Times (b,I)) = UsedI*Loc (I ";" (SubFrom (b,(intloc 0)))) by Th25
.= (UsedI*Loc I) \/ (UsedInt*Loc (SubFrom (b,(intloc 0)))) by SF_MASTR:46
.= (UsedI*Loc I) \/ {} by SF_MASTR:32
.= UsedI*Loc I ; :: thesis: verum