let p be preProgram of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (IncAddr p,k)
let k be Element of NAT ; :: thesis: UsedIntLoc p = UsedIntLoc (IncAddr p,k)
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 ) & UsedIntLoc p = Union (UIL * p) ) by Def2;
consider UIL2 being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) such that
A2: ( ( for i being Instruction of SCM+FSA holds UIL2 . i = UsedIntLoc i ) & UsedIntLoc (IncAddr p,k) = Union (UIL2 * (IncAddr p,k)) ) by Def2;
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 A1
.= UIL2 . c by A2 ; :: thesis: verum

end;

then A3: UIL = UIL2 by FUNCT_2:113;
set Ip = IncAddr p,k;
set f = UIL * (IncAddr p,k);
set g = UIL * p;

now

A4: dom (IncAddr p,k) = dom p by SCMFSA_4:def 6;
dom UIL = the Instructions of SCM+FSA by FUNCT_2:def 1;
then A5: ( rng p c= dom UIL & rng (IncAddr p,k) c= dom UIL ) by AMI_1:118;
then A6: dom (UIL * (IncAddr p,k)) = dom (IncAddr p,k) by RELAT_1:46;
hence dom (UIL * (IncAddr p,k)) = dom (UIL * p) by A4, A5, RELAT_1:46; :: 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 A7: x in dom (UIL * (IncAddr p,k)) ; :: thesis: (UIL * (IncAddr p,k)) . x = (UIL * p) . x
then (IncAddr p,k) . x in rng (IncAddr p,k) by A6, FUNCT_1:def 5;
then reconsider Ipx = (IncAddr p,k) . x as Instruction of SCM+FSA by A5, FUNCT_2:def 1;
p . x in rng p by A4, A6, A7, FUNCT_1:def 5;
then reconsider px = p . x as Instruction of SCM+FSA by A5, FUNCT_2:def 1;
dom p c= NAT by RELAT_1:def 18;
then reconsider x' = x as Instruction-Location of SCM+FSA by A4, A6, A7, AMI_1:def 4;
reconsider m = x' as Element of NAT by ORDINAL1:def 13;
A8: x' = insloc m ;
A9: (IncAddr p,k) . x = IncAddr (pi p,m),k by A4, A6, A7, A8, SCMFSA_4:def 6
.= IncAddr px,k by A4, A6, A7, AMI_1:def 47 ;
thus (UIL * (IncAddr p,k)) . x = UIL . Ipx by A7, FUNCT_1:22
.= UsedIntLoc Ipx by A1
.= UsedIntLoc px by A9, Th27
.= UIL . px by A2, A3
.= (UIL * p) . x by A4, A6, A7, FUNCT_1:23 ; :: thesis: verum

end;

hence UsedIntLoc p = UsedIntLoc (IncAddr p,k) by A1, A2, A3, FUNCT_1:9; :: thesis: verum