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