let p be preProgram of SCM+FSA ; :: thesis: for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (Shift p,k)
let k be Element of NAT ; :: thesis: UsedInt*Loc p = UsedInt*Loc (Shift p,k)
set Sp = Shift p,k;
consider UIL being Function of the Instructions 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;
consider UIL2 being Function of the Instructions 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 (Shift p,k) = Union (UIL2 * (Shift p,k)) by Def4;
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 A1
.= UIL2 . c by A3 ; :: thesis: verum

end;

then A5: UIL = UIL2 by FUNCT_2:113;
A6: 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
A7: x in dom (Shift p,k) and
A8: y = (Shift p,k) . x by FUNCT_1:def 5;
consider m being Element of NAT such that
A9: x = m + k and
A10: m in dom p by A6, A7;
(Shift p,k) . x = p . (insloc m) by A9, A10, VALUED_1:def 12;
hence y in rng p by A8, A10, 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
A11: x in dom p and
A12: 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 A11, AMI_1:def 4;
reconsider m = x' as Element of NAT by ORDINAL1:def 13;
( insloc (m + k) in dom (Shift p,k) & (Shift p,k) . (insloc (m + k)) = p . (insloc m) ) by A6, A11, VALUED_1:def 12;
hence y in rng (Shift p,k) by A12, FUNCT_1:def 5; :: thesis: verum

end;

then A13: rng (Shift p,k) = rng p by TARSKI:2;
A14: Union (UIL * (Shift p,k)) = union (rng (UIL * (Shift p,k))) by CARD_3:def 4;
rng (UIL * (Shift p,k)) = UIL .: (rng (Shift p,k)) by RELAT_1:160
.= rng (UIL * p) by A13, RELAT_1:160 ;
hence UsedInt*Loc p = UsedInt*Loc (Shift p,k) by A2, A4, A5, A14, CARD_3:def 4; :: thesis: verum