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

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