let i be Instruction of SCM+FSA; :: thesis: for J being Program of {INT,(INT *)} holds UsedInt*Loc (i ';' J) = (UsedInt*Loc i) \/ (UsedInt*Loc J)
let J be Program of {INT,(INT *)}; :: thesis: UsedInt*Loc (i ';' J) = (UsedInt*Loc i) \/ (UsedInt*Loc J)
thus UsedInt*Loc (i ';' J) = (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc J) by Th47
.= (UsedInt*Loc i) \/ (UsedInt*Loc J) by Th48 ; :: thesis: verum