let S be COM-Struct ; :: thesis: for P, Q being NAT -defined the InstructionsF of S -valued finite Function
for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
let P, Q be NAT -defined the InstructionsF of S -valued finite Function; :: thesis: for k being Nat st P c= Q holds
Reloc (P,k) c= Reloc (Q,k)
let k be Nat; :: thesis: ( P c= Q implies Reloc (P,k) c= Reloc (Q,k) )
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: Reloc (P,k) c= Reloc (Q,k)
then A6: Shift (P,k) c= Shift (Q,k) by VALUED_1:20;
A7: dom P c= dom Q by A5, GRFUNC_1:2;

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

let x be object ; :: thesis: ( x in dom (Reloc (P,k)) implies (Reloc (P,k)) . x = (Reloc (Q,k)) . x )
assume x in dom (Reloc (P,k)) ; :: thesis: (Reloc (P,k)) . x = (Reloc (Q,k)) . x
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: verum

end;

A14: dom (Shift (P,k)) c= dom (Shift (Q,k)) by A6, GRFUNC_1:2;

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

let x be object ; :: thesis: ( x in dom (Reloc (P,k)) implies x in dom (Reloc (Q,k)) )
assume x in dom (Reloc (P,k)) ; :: thesis: x in dom (Reloc (Q,k))
then x in dom (Shift (P,k)) by Th20;
then x in dom (Shift (Q,k)) by A14;
hence x in dom (Reloc (Q,k)) by Th20; :: thesis: verum

end;

then dom (Reloc (P,k)) c= dom (Reloc (Q,k)) ;
hence Reloc (P,k) c= Reloc (Q,k) by A8, GRFUNC_1:2; :: thesis: verum