let P, Q be Function; :: thesis: for k being Nat st P c= Q holds
Shift (P,k) c= Shift (Q,k)
let k be 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:2;
A3: dom (Shift (P,k)) = { (m + k) where m is Nat : m in dom P } by Def12;
A4: dom (Shift (Q,k)) = { (m + k) where m is Nat : m in dom Q } by Def12;

A5: now :: thesis: for x being object st x in dom (Shift (P,k)) holds
x in dom (Shift (Q,k))

let x be object ; :: 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 ex m1 being Nat st
( x = m1 + k & m1 in dom P ) by A3;
hence x in dom (Shift (Q,k)) by A2, A4; :: thesis: verum

end;

now :: thesis: for x being object st x in dom (Shift (P,k)) holds
(Shift (P,k)) . x = (Shift (Q,k)) . x

let x be object ; :: 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 Nat such that
A6: x = m1 + k and
A7: m1 in dom P by A3;
thus (Shift (P,k)) . x = (Shift (P,k)) . (m1 + k) by A6
.= P . m1 by A7, Def12
.= Q . m1 by A1, A7, GRFUNC_1:2
.= (Shift (Q,k)) . (m1 + k) by A2, A7, Def12
.= (Shift (Q,k)) . x by A6 ; :: thesis: verum

end;

hence Shift (P,k) c= Shift (Q,k) by A5, GRFUNC_1:2, TARSKI:def 3; :: thesis: verum