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

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