let i be Instruction of SCM+FSA; :: thesis: for J being Program of holds UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedI*Loc J)

let J be Program of ; :: thesis: UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedI*Loc J)

thus UsedI*Loc (i ";" J) = (UsedI*Loc (Macro i)) \/ (UsedI*Loc J) by Th43

.= (UsedInt*Loc i) \/ (UsedI*Loc J) by Th44 ; :: thesis: verum

let J be Program of ; :: thesis: UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedI*Loc J)

thus UsedI*Loc (i ";" J) = (UsedI*Loc (Macro i)) \/ (UsedI*Loc J) by Th43

.= (UsedInt*Loc i) \/ (UsedI*Loc J) by Th44 ; :: thesis: verum