let S be standard-ins homogeneous regular J/A-independent COM-Struct ; :: thesis:
let P, Q be NAT -defined the Instructions of S -valued finite Function; :: thesis:
let k be Nat; :: thesis:
set rP = Reloc (P,k);
set rQ = Reloc (Q,k);
A1: dom (Reloc (P,k)) = { (m + k) where m is Element of NAT : m in dom P } by Th117;
A2: dom (Shift (P,k)) = { (m + k) where m is Element of NAT : m in dom P } by VALUED_1:def 12;
A3: dom (Shift (Q,k)) = { (m + k) where m is Element of NAT : m in dom Q } by VALUED_1:def 12;
assume A4: P c= Q ; :: thesis:
then A5: Shift (P,k) c= Shift (Q,k) by VALUED_1:20;
A6: dom P c= dom Q by A4, GRFUNC_1:2;

let x be set ; :: thesis:
assume x in dom (Reloc (P,k)) ; :: thesis:
then consider m1 being Element of NAT such that
A8: x = m1 + k and
A9: m1 in dom P by A1;
A10: m1 + k in dom (Shift (Q,k)) by A6, A3, A9;
A11: m1 + k in dom (Shift (P,k)) by A2, A9;
then A12: (Shift (P,k)) /. (m1 + k) = (Shift (P,k)) . (m1 + k) by PARTFUN1:def 6
.= (Shift (Q,k)) . (m1 + k) by A5, A11, GRFUNC_1:2
.= (Shift (Q,k)) /. (m1 + k) by A10, PARTFUN1:def 6 ;
thus (Reloc (P,k)) . x = IncAddr (((Shift (Q,k)) /. (m1 + k)),k) by A11, A12, Def40, A8
.= (Reloc (Q,k)) . x by A8, A10, Def40 ; :: thesis:

end;

end;