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