let i be Instruction of SCM+FSA ; :: thesis:
consider UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A1: for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i and
A2: UsedIntLoc (Macro i) = Union (UIL * (Macro i)) by Def2;
A3: ( rng (Macro i) = {i,(halt SCM+FSA )} & dom UIL = the Instructions of SCM+FSA ) by FUNCT_2:def 1, FUNCT_4:67;
thus UsedIntLoc (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
.= (UsedIntLoc i) \/ (UIL . (halt SCM+FSA )) by A1
.= (UsedIntLoc i) \/ (UsedIntLoc (halt SCM+FSA )) by A1
.= UsedIntLoc i by Th17 ; :: thesis: