let i be Instruction of SCM+FSA; :: thesis: UsedILoc (Macro i) = UsedIntLoc i
rng (Macro i) = {i,(halt SCM+FSA)} by COMPOS_1:67;
hence UsedILoc (Macro i) = union { (UsedIntLoc j) where j is Instruction of SCM+FSA : j in {i,(halt SCM+FSA)} }
.= (UsedIntLoc i) \/ (UsedIntLoc (halt SCM+FSA)) from SUBSET_1:sch 6()
.= UsedIntLoc i by Th13 ;
:: thesis: verum