let j be Instruction of SCM+FSA; :: thesis: for I being Program of holds UsedI*Loc (I ";" j) = (UsedI*Loc I) \/ (UsedInt*Loc j)
let I be Program of ; :: thesis: UsedI*Loc (I ";" j) = (UsedI*Loc I) \/ (UsedInt*Loc j)
thus UsedI*Loc (I ";" j) = (UsedI*Loc I) \/ (UsedI*Loc (Macro j)) by Th43
.= (UsedI*Loc I) \/ (UsedInt*Loc j) by Th44 ; :: thesis: verum