let
p
be
preProgram
of
SCM+FSA
;
:: thesis:
for
k
being
Nat
holds
UsedI*Loc
p
=
UsedI*Loc
(
Shift
(
p
,
k
)
)
let
k
be
Nat
;
:: thesis:
UsedI*Loc
p
=
UsedI*Loc
(
Shift
(
p
,
k
)
)
dom
p
c=
NAT
;
then
rng
p
=
rng
(
Shift
(
p
,
k
)
)
by
VALUED_1:26
;
hence
UsedI*Loc
p
=
UsedI*Loc
(
Shift
(
p
,
k
)
)
;
:: thesis:
verum