let k be Element of NAT ; :: thesis:
let R be good Ring; :: thesis:
let p be FinPartState of (SCM R); :: thesis:
assume A1: not R is trivial ; :: thesis:
let F be PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)); :: thesis:
assume that
A2: IC (SCM R) in dom p and
A3: F is data-only ; :: thesis:
F1: (ProgramPart p) +* p = p by FUNCT_4:119;
F2: (ProgramPart (Relocated p,k)) +* (Relocated p,k) = Relocated p,k by FUNCT_4:119;

hereby :: thesis:

assume A4: ProgramPart p,p computes F ; :: thesis:
thus ProgramPart (Relocated p,k), Relocated p,k computes F :: thesis:

let x be set ; :: according to AMI_1:def 30 :: thesis:
assume A5: x in dom F ; :: thesis:
then consider d1 being FinPartState of (SCM R) such that
A6: x = d1 and
A7: ((ProgramPart p) +* p) +* d1 is pre-program of SCM R and
A8: F . d1 c= Result (ProgramPart p),(p +* d1) by A4, AMI_1:def 30;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider d = x as FinPartState of (SCM R) by A5, COMPOS_1:25;
reconsider d = d as data-only FinPartState of (SCM R) by A3, A5, COMPOS_1:def 24;
X: Relocated (p +* d),k = (Relocated p,k) +* d by AMISTD_2:78;
xx: dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
y: ProgramPart ((Relocated p,k) +* d) = ProgramPart (Relocated p,k) by xx, FUNCT_4:76;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A9: IC (SCM R) in dom (p +* d) by A2, XBOOLE_0:def 3;
then A10: DataPart (Result (ProgramPart p),(p +* d1)) = DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d)) by A1, A6, A7, Th41, F1, x, X, y;
reconsider Fd1 = F . d1 as FinPartState of (SCM R) by A8;
take d ; :: thesis:
thus x = d ; :: thesis:
(Relocated p,k) +* d = Relocated (p +* d),k by AMISTD_2:78;
hence ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d is pre-program of SCM R by A1, A6, A7, A9, Th36, F1, F2, Th40; :: thesis:
A11: Fd1 is data-only by A3, A5, A6, COMPOS_1:def 24;
then F . d1 c= DataPart (Result (ProgramPart p),(p +* d1)) by A8, COMPOS_1:17;
hence F . d c= Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d) by A6, A11, A10, COMPOS_1:17; :: thesis:

end;

end;

assume A12: ProgramPart (Relocated p,k), Relocated p,k computes F ; :: thesis:
let x be set ; :: according to AMI_1:def 30 :: thesis:
assume A13: x in dom F ; :: thesis:
then consider d1 being FinPartState of (SCM R) such that
A14: x = d1 and
A15: ((ProgramPart (Relocated p,k)) +* (Relocated p,k)) +* d1 is pre-program of SCM R and
A16: F . d1 c= Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1) by A12, AMI_1:def 30;
dom F c= FinPartSt (SCM R) by RELAT_1:def 18;
then reconsider d = x as FinPartState of (SCM R) by A13, COMPOS_1:25;
reconsider d = d as data-only FinPartState of (SCM R) by A3, A13, COMPOS_1:def 24;
dom (p +* d) = (dom p) \/ (dom d) by FUNCT_4:def 1;
then A17: IC (SCM R) in dom (p +* d) by A2, XBOOLE_0:def 3;
A18: (Relocated p,k) +* d = Relocated (p +* d),k by AMISTD_2:78;
then A19: p +* d is autonomic by A1, A14, A15, A17, Th40, F2;
then A20: p +* d is halting by A1, A14, A15, A18, A17, Th36, F2;
X: Relocated (p +* d),k = (Relocated p,k) +* d by AMISTD_2:78;
xx: dom d misses NAT by COMPOS_1:40;
then x: ProgramPart (p +* d) = ProgramPart p by FUNCT_4:76;
y: ProgramPart ((Relocated p,k) +* d) = ProgramPart (Relocated p,k) by xx, FUNCT_4:76;
A21: DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1)) = DataPart (Result (ProgramPart p),(p +* d)) by A1, A17, A19, A20, Th41, x, y, X, A14;
take d ; :: thesis:
thus x = d ; :: thesis:
thus ((ProgramPart p) +* p) +* d is pre-program of SCM R by A1, A14, A15, A18, A17, A19, Th36, F1, F2; :: thesis:
reconsider Fd1 = F . d1 as FinPartState of (SCM R) by A16;
A22: Fd1 is data-only by A3, A13, A14, COMPOS_1:def 24;
then F . d1 c= DataPart (Result (ProgramPart (Relocated p,k)),((Relocated p,k) +* d1)) by A16, COMPOS_1:17;
hence F . d c= Result (ProgramPart p),(p +* d) by A14, A22, A21, COMPOS_1:17; :: thesis: