let p be preProgram of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (Shift p,k)
let k be Element of NAT ; :: thesis: UsedIntLoc p = UsedIntLoc (Shift 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 (Shift p,k) = Union (UIL2 * (Shift 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 Sp = Shift p,k;
A4: Union (UIL * (Shift p,k)) = union (rng (UIL * (Shift p,k))) by CARD_3:def 4;
A5: dom (Shift p,k) = { (m + k) where m is Element of NAT : m in dom p } by VALUED_1:def 12;

now

let y be set ; :: thesis: ( ( y in rng (Shift p,k) implies y in rng p ) & ( y in rng p implies y in rng (Shift p,k) ) )

hereby :: thesis: ( y in rng p implies y in rng (Shift p,k) )

assume y in rng (Shift p,k) ; :: thesis: y in rng p
then consider x being set such that
A6: ( x in dom (Shift p,k) & y = (Shift p,k) . x ) by FUNCT_1:def 5;
consider m being Element of NAT such that
A7: ( x = m + k & m in dom p ) by A5, A6;
(Shift p,k) . x = p . (insloc m) by A7, VALUED_1:def 12;
hence y in rng p by A6, A7, FUNCT_1:def 5; :: thesis: verum

end;

assume y in rng p ; :: thesis: y in rng (Shift p,k)
then consider x being set such that
A8: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
dom p c= NAT by RELAT_1:def 18;
then reconsider x' = x as Instruction-Location of SCM+FSA by A8, AMI_1:def 4;
reconsider m = x' as Element of NAT by ORDINAL1:def 13;
A10: insloc (m + k) in dom (Shift p,k) by A5, A8;
(Shift p,k) . (insloc (m + k)) = p . (insloc m) by A8, VALUED_1:def 12;
hence y in rng (Shift p,k) by A8, A10, FUNCT_1:def 5; :: thesis: verum

end;

then A11: rng (Shift p,k) = rng p by TARSKI:2;
rng (UIL * (Shift p,k)) = UIL .: (rng (Shift p,k)) by RELAT_1:160
.= rng (UIL * p) by A11, RELAT_1:160 ;
hence UsedIntLoc p = UsedIntLoc (Shift p,k) by A1, A2, A3, A4, CARD_3:def 4; :: thesis: verum