let i, j be Instruction of SCM+FSA; :: thesis: UsedIntLoc (i ';' j) = (UsedIntLoc i) \/ (UsedIntLoc j)
thus UsedIntLoc (i ';' j) = (UsedIntLoc (Macro i)) \/ (UsedIntLoc (Macro j)) by Th31
.= (UsedIntLoc (Macro i)) \/ (UsedIntLoc j) by Th32
.= (UsedIntLoc i) \/ (UsedIntLoc j) by Th32 ; :: thesis: verum