let p be preProgram of SCM+FSA; :: thesis: for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k))
let k be Element of NAT ; :: thesis: UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k))
set Ip = IncAddr (p,k);
consider UIL being Function of the InstructionsF 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 p = Union (UIL * p) by Def4;
set g = UIL * p;
set f = UIL * (IncAddr (p,k));
consider UIL2 being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) such that
A3: for i being Instruction of SCM+FSA holds UIL2 . i = UsedInt*Loc i and
A4: UsedInt*Loc (IncAddr (p,k)) = Union (UIL2 * (IncAddr (p,k))) by Def4;
for c being Element of the InstructionsF of SCM+FSA holds UIL . c = UIL2 . c

proof

let c be Element of the InstructionsF of SCM+FSA; :: thesis: UIL . c = UIL2 . c
reconsider d = c as Instruction of SCM+FSA ;
thus UIL . c = UsedInt*Loc d by A1
.= UIL2 . c by A3 ; :: thesis: verum

end;

then A5: UIL = UIL2 by FUNCT_2:63;

now :: thesis: ( dom (UIL * (IncAddr (p,k))) = dom (UIL * p) & ( for x being set st x in dom (UIL * (IncAddr (p,k))) holds
(UIL * (IncAddr (p,k))) . x = (UIL * p) . x ) )

A6: dom UIL = the InstructionsF of SCM+FSA by FUNCT_2:def 1;
then A7: rng p c= dom UIL ;
rng (IncAddr (p,k)) c= dom UIL by A6;
then A8: dom (UIL * (IncAddr (p,k))) = dom (IncAddr (p,k)) by RELAT_1:27;
A9: dom (IncAddr (p,k)) = dom p by COMPOS_1:def 21;
hence dom (UIL * (IncAddr (p,k))) = dom (UIL * p) by A7, A8, RELAT_1:27; :: thesis: for x being set st x in dom (UIL * (IncAddr (p,k))) holds
(UIL * (IncAddr (p,k))) . x = (UIL * p) . x
let x be set ; :: thesis: ( x in dom (UIL * (IncAddr (p,k))) implies (UIL * (IncAddr (p,k))) . x = (UIL * p) . x )
assume A10: x in dom (UIL * (IncAddr (p,k))) ; :: thesis: (UIL * (IncAddr (p,k))) . x = (UIL * p) . x
then p . x in rng p by A9, A8, FUNCT_1:def 3;
then reconsider px = p . x as Instruction of SCM+FSA ;
reconsider x9 = x as Element of NAT by A8, A10;
reconsider m = x9 as Element of NAT ;
A11: (IncAddr (p,k)) . x = IncAddr ((p /. m),k) by A9, A8, A10, COMPOS_1:def 21
.= IncAddr (px,k) by A9, A8, A10, PARTFUN1:def 6 ;
(IncAddr (p,k)) . x in rng (IncAddr (p,k)) by A8, A10, FUNCT_1:def 3;
then reconsider Ipx = (IncAddr (p,k)) . x as Instruction of SCM+FSA ;
thus (UIL * (IncAddr (p,k))) . x = UIL . Ipx by A10, FUNCT_1:12
.= UsedInt*Loc Ipx by A1
.= UsedInt*Loc px by A11, Th39
.= UIL . px by A3, A5
.= (UIL * p) . x by A9, A8, A10, FUNCT_1:13 ; :: thesis: verum

end;

hence UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k)) by A2, A4, A5, FUNCT_1:2; :: thesis: verum