let P, Q be Function; :: thesis: for k being Element of NAT st P c= Q holds
Shift P,k c= Shift Q,k
let k be Element of NAT ; :: thesis: ( P c= Q implies Shift P,k c= Shift Q,k )
assume A1: P c= Q ; :: thesis: Shift P,k c= Shift Q,k
then A2: dom P c= dom Q by GRFUNC_1:8;
A3: dom (Shift P,k) = { (m + k) where m is Element of NAT : m in dom P } by Def12;
A4: dom (Shift Q,k) = { (m + k) where m is Element of NAT : m in dom Q } by Def12;

now

let x be set ; :: thesis: ( x in dom (Shift P,k) implies x in dom (Shift Q,k) )
assume x in dom (Shift P,k) ; :: thesis: x in dom (Shift Q,k)
then consider m1 being Element of NAT such that
A5: ( x = m1 + k & m1 in dom P ) by A3;
thus x in dom (Shift Q,k) by A2, A4, A5; :: thesis: verum

end;

then A6: dom (Shift P,k) c= dom (Shift Q,k) by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in dom (Shift P,k) implies (Shift P,k) . x = (Shift Q,k) . x )
assume x in dom (Shift P,k) ; :: thesis: (Shift P,k) . x = (Shift Q,k) . x
then consider m1 being Element of NAT such that
A7: ( x = m1 + k & m1 in dom P ) by A3;
thus (Shift P,k) . x = (Shift P,k) . (m1 + k) by A7
.= P . m1 by A7, Def12
.= Q . m1 by A1, A7, GRFUNC_1:8
.= (Shift Q,k) . (m1 + k) by A2, A7, Def12
.= (Shift Q,k) . x by A7 ; :: thesis: verum

end;

hence Shift P,k c= Shift Q,k by A6, GRFUNC_1:8; :: thesis: verum