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) )
assume A1: P c= Q ; :: thesis: ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k)
set rP = Relocated P,k;
set rQ = Relocated Q,k;
A2: dom (ProgramPart (Relocated P,k)) = { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by SCMFSA_5:3;
A3: ProgramPart (Relocated P,k) = IncAddr [(Shift (ProgramPart P),k)],k by SCMFSA_5:2;
A4: ProgramPart (Relocated Q,k) = IncAddr [(Shift (ProgramPart Q),k)],k by SCMFSA_5:2;
A5: ProgramPart P c= ProgramPart Q by A1, RELAT_1:105;
then A6: Shift (ProgramPart P),k c= Shift (ProgramPart Q),k by VALUED_1:21;
then A7: dom (Shift (ProgramPart P),k) c= dom (Shift (ProgramPart Q),k) by GRFUNC_1:8;
A8: dom (ProgramPart P) c= dom (ProgramPart Q) 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 A3, SCMFSA_4:def 6;
then x in dom (Shift (ProgramPart Q),k) by A7;
hence x in dom (ProgramPart (Relocated Q,k)) by A4, SCMFSA_4:def 6; :: thesis: verum

end;

then A9: dom (ProgramPart (Relocated P,k)) c= dom (ProgramPart (Relocated Q,k)) by TARSKI:def 3;
A10: dom (Shift (ProgramPart P),k) = { (m + k) where m is Element of NAT : m in dom (ProgramPart P) } by VALUED_1:def 12;
A11: dom (Shift (ProgramPart Q),k) = { (m + k) where m is Element of NAT : m in dom (ProgramPart Q) } by VALUED_1:def 12;

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
A12: ( x = m1 + k & m1 in dom (ProgramPart P) ) by A2;
A13: ( insloc (m1 + k) in dom (Shift (ProgramPart P),k) & insloc (m1 + k) in dom (Shift (ProgramPart Q),k) ) by A8, A10, A11, A12;
then A14: pi [(Shift (ProgramPart P),k)],(m1 + k) = (Shift (ProgramPart P),k) . (insloc (m1 + k)) by AMI_1:def 47
.= (Shift (ProgramPart Q),k) . (insloc (m1 + k)) by A6, A13, GRFUNC_1:8
.= pi [(Shift (ProgramPart Q),k)],(m1 + k) by A13, AMI_1:def 47 ;
thus (ProgramPart (Relocated P,k)) . x = (IncAddr [(Shift (ProgramPart P),k)],k) . (insloc (m1 + k)) by A12, SCMFSA_5:2
.= IncAddr (pi [(Shift (ProgramPart Q),k)],(m1 + k)),k by A13, A14, SCMFSA_4:def 6
.= (IncAddr [(Shift (ProgramPart Q),k)],k) . (insloc (m1 + k)) by A13, SCMFSA_4:def 6
.= (ProgramPart (Relocated Q,k)) . x by A12, SCMFSA_5:2 ; :: thesis: verum

end;

hence ProgramPart (Relocated P,k) c= ProgramPart (Relocated Q,k) by A9, GRFUNC_1:8; :: thesis: verum