let i, j be Instruction of SCM+FSA; :: thesis: UsedInt*Loc (i ";" j) = (UsedInt*Loc i) \/ (UsedInt*Loc j)
thus UsedInt*Loc (i ";" j) = (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc (Macro j)) by Th43
.= (UsedInt*Loc (Macro i)) \/ (UsedInt*Loc j) by Th44
.= (UsedInt*Loc i) \/ (UsedInt*Loc j) by Th44 ; :: thesis: verum