let S be COM-Struct ; :: thesis:
let P, Q be NAT -defined the InstructionsF 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 Nat : m in dom P } by Th21;
A2: dom (Shift (P,k)) = { (m + k) where m is Nat : m in dom P } by VALUED_1:def 12;
A3: dom (Shift (Q,k)) = { (m + k) where m is Nat : m in dom Q } by VALUED_1:def 12;
A4: Reloc (Q,k) = IncAddr ((Shift (Q,k)),k) by Th22;
assume A5: P c= Q ; :: thesis:
then A6: Shift (P,k) c= Shift (Q,k) by VALUED_1:20;
A7: dom P c= dom Q by A5, GRFUNC_1:2;

let x be object ; :: thesis:
assume x in dom (Reloc (P,k)) ; :: thesis:
then consider m1 being Nat such that
A9: x = m1 + k and
A10: m1 in dom P by A1;
A11: m1 + k in dom (Shift (Q,k)) by A7, A3, A10;
A12: m1 + k in dom (Shift (P,k)) by A2, A10;
then A13: (Shift (P,k)) /. (m1 + k) = (Shift (P,k)) . (m1 + k) by PARTFUN1:def 6
.= (Shift (Q,k)) . (m1 + k) by A6, A12, GRFUNC_1:2
.= (Shift (Q,k)) /. (m1 + k) by A11, PARTFUN1:def 6 ;
thus (Reloc (P,k)) . x = (IncAddr ((Shift (P,k)),k)) . x by Th22
.= IncAddr (((Shift (Q,k)) /. (m1 + k)),k) by A12, A13, A9, Def9
.= (Reloc (Q,k)) . x by A9, A11, A4, Def9 ; :: thesis:

end;

end;