let P, Q be FinPartState of SCM+FSA; :: thesis: for k being Element of NAT st P c= Q holds
ProgramPart (Relocated (P,k)) c= ProgramPart (Relocated (Q,k))
let k be Element of NAT ; :: thesis: ( P c= Q implies ProgramPart (Relocated (P,k)) c= ProgramPart (Relocated (Q,k)) )
set rP = Relocated (P,k);
set rQ = Relocated (Q,k);
A1: dom (ProgramPart (Relocated (P,k))) = dom (Reloc ((ProgramPart P),k)) by COMPOS_1:116
.= { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by COMPOS_1:117 ;
A2: dom (Shift ((ProgramPart P),k)) = { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by VALUED_1:def 12;
A3: dom (Shift ((ProgramPart Q),k)) = { (m + k) where m is Element of NAT : m in dom (ProgramPart Q) } by VALUED_1:def 12;
assume P c= Q ; :: thesis: ProgramPart (Relocated (P,k)) c= ProgramPart (Relocated (Q,k))
then A4: ProgramPart P c= ProgramPart Q by RELAT_1:105;
then A5: Shift ((ProgramPart P),k) c= Shift ((ProgramPart Q),k) by VALUED_1:21;
A6: dom (ProgramPart P) c= dom (ProgramPart Q) by A4, GRFUNC_1:8;

A7: now

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

end;

A13: ProgramPart (Relocated (Q,k)) = Reloc ((ProgramPart Q),k) by COMPOS_1:116;
A14: ProgramPart (Relocated (P,k)) = Reloc ((ProgramPart P),k) by COMPOS_1:116;
A15: dom (Shift ((ProgramPart P),k)) c= dom (Shift ((ProgramPart Q),k)) by A5, GRFUNC_1:8;

now

let x be set ; :: thesis: ( x in dom (ProgramPart (Relocated (P,k))) implies x in dom (ProgramPart (Relocated (Q,k))) )
assume x in dom (ProgramPart (Relocated (P,k))) ; :: thesis: x in dom (ProgramPart (Relocated (Q,k)))
then x in dom (Shift ((ProgramPart P),k)) by A14, COMPOS_1:def 40;
then x in dom (Shift ((ProgramPart Q),k)) by A15;
hence x in dom (ProgramPart (Relocated (Q,k))) by A13, COMPOS_1:def 40; :: thesis: verum

end;

then dom (ProgramPart (Relocated (P,k))) c= dom (ProgramPart (Relocated (Q,k))) by TARSKI:def 3;
hence ProgramPart (Relocated (P,k)) c= ProgramPart (Relocated (Q,k)) by A7, GRFUNC_1:8; :: thesis: verum