let i, j be Instruction of SCM+FSA; :: thesis: UsedILoc (i ";" j) = (UsedIntLoc i) \/ (UsedIntLoc j)
thus UsedILoc (i ";" j) = (UsedILoc (Macro i)) \/ (UsedILoc (Macro j)) by Th27
.= (UsedILoc (Macro i)) \/ (UsedIntLoc j) by Th28
.= (UsedIntLoc i) \/ (UsedIntLoc j) by Th28 ; :: thesis: verum