let i be Instruction of SCM+FSA; :: thesis: UsedInt*Loc (Macro i) = UsedInt*Loc i
consider UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A1: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and
A2: UsedInt*Loc (Macro i) = Union (UIL * (Macro i)) by Def4;
A3: ( rng (Macro i) = {i,(halt SCM+FSA)} & dom UIL = the Instructions of SCM+FSA ) by FUNCT_2:def 1, FUNCT_4:67;
thus UsedInt*Loc (Macro i) = union (rng (UIL * (Macro i))) by A2, CARD_3:def 4
.= union (UIL .: (rng (Macro i))) by RELAT_1:160
.= union {(UIL . i),(UIL . (halt SCM+FSA))} by A3, FUNCT_1:118
.= (UIL . i) \/ (UIL . (halt SCM+FSA)) by ZFMISC_1:93
.= (UsedInt*Loc i) \/ (UIL . (halt SCM+FSA)) by A1
.= (UsedInt*Loc i) \/ (UsedInt*Loc (halt SCM+FSA)) by A1
.= (UsedInt*Loc i) \/ {} by Th36
.= UsedInt*Loc i ; :: thesis: verum