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