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