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, COMPOS_1:67;
thus UsedIntLoc (Macro i) = union (rng (UIL * (Macro i))) by A2, CARD_3:def 4
.= union (UIL .: (rng (Macro i))) by RELAT_1:127
.= union {(UIL . i),(UIL . (halt SCM+FSA))} by A3, FUNCT_1:60
.= (UIL . i) \/ (UIL . (halt SCM+FSA)) by ZFMISC_1:75
.= (UsedIntLoc i) \/ (UIL . (halt SCM+FSA)) by A1
.= (UsedIntLoc i) \/ (UsedIntLoc (halt SCM+FSA)) by A1
.= UsedIntLoc i by Th17 ; :: thesis: