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 ) & UsedInt*Loc (Macro i) = Union (UIL * (Macro i)) ) by Def4;
A2: rng (Macro i) = {i,(halt SCM+FSA )} by FUNCT_4:67;
A3: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
thus UsedInt*Loc (Macro i) = union (rng (UIL * (Macro i))) by A1, CARD_3:def 4
.= union (UIL .: (rng (Macro i))) by RELAT_1:160
.= union {(UIL . i),(UIL . (halt SCM+FSA ))} by A2, 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