let l be Element of NAT ; :: thesis: for i being Instruction of SCM+FSA holds UsedIntLoc (l .--> i) = UsedIntLoc i
let i be Instruction of SCM+FSA; :: thesis: UsedIntLoc (l .--> i) = UsedIntLoc i
set p = l .--> i;
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 (l .--> i) = Union (UIL * (l .--> i)) by SF_MASTR:def 2;
A3: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
thus UsedIntLoc (l .--> i) = union (rng (UIL * ({l} --> i))) by A2, CARD_3:def 4
.= union (rng ({l} --> (UIL . i))) by A3, FUNCOP_1:17
.= union {(UIL . i)} by FUNCOP_1:8
.= union {(UsedIntLoc i)} by A1
.= UsedIntLoc i by ZFMISC_1:25 ; :: thesis: verum