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 Th47
.= (UsedInt*Loc I) \/ (UsedInt*Loc j) by Th48 ; :: thesis: verum