let p be preProgram of SCM+FSA; :: thesis: for l being Element of NAT
for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedInt*Loc p = UsedInt*Loc (p +* (l .--> ic))
let l be Element of NAT ; :: thesis: for ic being Instruction of SCM+FSA st l in dom p & ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) holds
UsedInt*Loc p = UsedInt*Loc (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 & UsedInt*Loc pc = UsedInt*Loc ic ) implies UsedInt*Loc p = UsedInt*Loc (p +* (l .--> ic)) )
set pl = p +* (l .--> ic);
assume that
A1: l in dom p and
A2: ex pc being Instruction of SCM+FSA st
( pc = p . l & UsedInt*Loc pc = UsedInt*Loc ic ) ; :: thesis: UsedInt*Loc p = UsedInt*Loc (p +* (l .--> ic))
consider UIL being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A3: for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i and
A4: UsedInt*Loc p = Union (UIL * p) by SF_MASTR:def 4;
set f = UIL * p;
set g = UIL * (p +* (l .--> ic));
consider UIL2 being Function of the Instructions of SCM+FSA,(Fin FinSeq-Locations) such that
A5: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A6: UsedInt*Loc (p +* (l .--> ic)) = Union (UIL2 * (p +* (l .--> ic))) by SF_MASTR:def 4;
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 = UsedInt*Loc d by A3
.= UIL2 . c by A5 ; :: thesis: verum

end;

then A7: UIL = UIL2 by FUNCT_2:63;
A8: (p +* (l .--> ic)) . l = (p +* (l,ic)) . l by A1, FUNCT_7:def 3
.= ic by A1, FUNCT_7:31 ;

now

A9: dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then rng p c= dom UIL by RELAT_1:def 19;
then A10: dom (UIL * p) = dom p by RELAT_1:27;
A11: dom p = dom (p +* (l .--> ic)) by A1, FUNCT_7:112;
A12: rng (p +* (l .--> ic)) c= dom UIL by A9, RELAT_1:def 19;
hence dom (UIL * p) = dom (UIL * (p +* (l .--> ic))) by A11, A10, RELAT_1:27; :: 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 A13: 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 A11, A10, FUNCT_1:def 3;
then reconsider plx = (p +* (l .--> ic)) . x as Instruction of SCM+FSA by A12, 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:13;
then p . x = (p +* (l .--> ic)) . x by FUNCT_4:11;
hence (UIL * p) . x = UIL . plx by A13, FUNCT_1:12
.= (UIL * (p +* (l .--> ic))) . x by A11, A10, A13, FUNCT_1:13 ;
:: thesis: verum

end;

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

thus (UIL * p) . x = UIL . (p . x) by A13, FUNCT_1:12
.= UsedInt*Loc plx by A2, A8, A3, A14
.= UIL . plx by A5, A7
.= (UIL * (p +* (l .--> ic))) . x by A11, A10, A13, FUNCT_1:13 ; :: thesis: verum

end;

end;

end;

hence UsedInt*Loc p = UsedInt*Loc (p +* (l .--> ic)) by A4, A6, A7, FUNCT_1:2; :: thesis: verum