let p be preProgram of SCM+FSA ; :: thesis: for l being Instruction-Location of SCM+FSA
for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds
UsedIntLoc p = UsedIntLoc (p +* (l .--> ic))
let l be Instruction-Location of SCM+FSA ; :: thesis: for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) holds
UsedIntLoc p = UsedIntLoc (p +* (l .--> ic))
let ic be Instruction of SCM+FSA ; :: thesis: ( l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) implies UsedIntLoc p = UsedIntLoc (p +* (l .--> ic)) )
set pl = p +* (l .--> ic);
assume A1: ( l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedIntLoc pc = UsedIntLoc ic ) ) ; :: thesis: UsedIntLoc p = UsedIntLoc (p +* (l .--> ic))
then A2: (p +* (l .--> ic)) . l = (p +* l,ic) . l by FUNCT_7:def 3
.= ic by A1, FUNCT_7:33 ;
consider UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A3: ( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & UsedIntLoc p = Union (UIL * p) ) by SF_MASTR:def 2;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A4: ( ( for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i ) & UsedIntLoc (p +* (l .--> ic)) = Union (UIL2 * (p +* (l .--> ic))) ) by SF_MASTR:def 2;
for c being Element of the Instructions of SCM+FSA holds UIL . c = UIL2 . c

proof

let c be Element of the Instructions of SCM+FSA ; :: thesis: UIL . c = UIL2 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedIntLoc d by A3
.= UIL2 . c by A4 ; :: thesis: verum

end;

then A5: UIL = UIL2 by FUNCT_2:113;
set f = UIL * p;
set g = UIL * (p +* (l .--> ic));

now

A6: dom p = dom (p +* (l .--> ic)) by A1, FUNCT_7:114;
dom p c= NAT by RELAT_1:def 18;
then B: p +* (l .--> ic) is NAT -defined by A6, RELAT_1:def 18;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then A7: ( rng p c= dom UIL & rng (p +* (l .--> ic)) c= dom UIL ) by AMI_1:118, B;
then A8: dom (UIL * p) = dom p by RELAT_1:46;
hence dom (UIL * p) = dom (UIL * (p +* (l .--> ic))) by A6, A7, RELAT_1:46; :: thesis: for x being set st x in dom (UIL * p) holds
(UIL * p) . b₂ = (UIL * (p +* (l .--> ic))) . b₂
let x be set ; :: thesis: ( x in dom (UIL * p) implies (UIL * p) . b₁ = (UIL * (p +* (l .--> ic))) . b₁ )
assume A9: x in dom (UIL * p) ; :: thesis: (UIL * p) . b₁ = (UIL * (p +* (l .--> ic))) . b₁
then (p +* (l .--> ic)) . x in rng (p +* (l .--> ic)) by A6, A8, FUNCT_1:def 5;
then reconsider plx = (p +* (l .--> ic)) . x as Instruction of SCM+FSA by A7, FUNCT_2:def 1;

per cases ( x <> l or x = l ) ;

suppose x <> l ; :: thesis: (UIL * p) . b₁ = (UIL * (p +* (l .--> ic))) . b₁

then not x in {l} by TARSKI:def 1;
then not x in dom (l .--> ic) by FUNCOP_1:19;
then p . x = (p +* (l .--> ic)) . x by FUNCT_4:12;
hence (UIL * p) . x = UIL . plx by A9, FUNCT_1:22
.= (UIL * (p +* (l .--> ic))) . x by A6, A8, A9, FUNCT_1:23 ;
:: thesis: verum

end;

suppose A10: x = l ; :: thesis: (UIL * p) . b₁ = (UIL * (p +* (l .--> ic))) . b₁

thus (UIL * p) . x = UIL . (p . x) by A9, FUNCT_1:22
.= UsedIntLoc plx by A1, A2, A3, A10
.= UIL . plx by A4, A5
.= (UIL * (p +* (l .--> ic))) . x by A6, A8, A9, FUNCT_1:23 ; :: thesis: verum

end;

end;

end;

hence UsedIntLoc p = UsedIntLoc (p +* (l .--> ic)) by A3, A4, A5, FUNCT_1:9; :: thesis: verum