set A = { (m + k) where m is Element of NAT : m in dom p } ;
set B = { m where m is Element of NAT : m in dom p } ;
set f = Shift p,k;
A1:
dom (Shift p,k) = { (m + k) where m is Element of NAT : m in dom p }
by VALUED_1:def 12;
A2:
{ (m + k) where m is Element of NAT : m in dom p } c= NAT
NAT c= the carrier of S
by AMI_1:def 3;
then A3:
dom (Shift p,k) c= the carrier of S
by A1, A2, XBOOLE_1:1;
for x being set st x in dom (Shift p,k) holds
(Shift p,k) . x in the Object-Kind of S . x
proof
let x be
set ;
( x in dom (Shift p,k) implies (Shift p,k) . x in the Object-Kind of S . x )
assume A4:
x in dom (Shift p,k)
;
(Shift p,k) . x in the Object-Kind of S . x
then
x in { (m + k) where m is Element of NAT : m in dom p }
by VALUED_1:def 12;
then consider m being
Element of
NAT such that A5:
x = m + k
and A6:
m in dom p
;
A7:
(Shift p,k) . x = p . m
by A5, A6, VALUED_1:def 12;
reconsider y =
x as
Element of
NAT by A1, A2, A4;
A8:
the
Object-Kind of
S . y = the
Instructions of
S
by AMI_1:def 14;
consider s being
State of
S such that A9:
p c= s
by PBOOLE:156;
A10:
ex
j being
Element of
NAT st
(
m + k = j + k &
j in dom p )
by A1, A4, A5;
reconsider m =
m as
Element of
NAT ;
s . m in the
Instructions of
S
;
hence
(Shift p,k) . x in the
Object-Kind of
S . x
by A7, A8, A9, A10, GRFUNC_1:8;
verum
end;
hence
Shift p,k is PartState of S
by A3, FUNCT_1:def 20, RELAT_1:def 18; verum