let p be FinPartState of SCM ; :: thesis: for k being Element of NAT holds ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k
let k be Element of NAT ; :: thesis: ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k
set X = (Start-At ((IC p) + k),SCM ) | NAT ;
consider x being Element of dom ((Start-At ((IC p) + k),SCM ) | NAT );

A1: now

assume (Start-At ((IC p) + k),SCM ) | NAT <> {} ; :: thesis: contradiction
then dom ((Start-At ((IC p) + k),SCM ) | NAT ) <> {} ;
then x in dom ((Start-At ((IC p) + k),SCM ) | NAT ) ;
then A2: x in (dom (Start-At ((IC p) + k),SCM )) /\ NAT by RELAT_1:90;
then x in NAT by XBOOLE_0:def 4;
then reconsider x = x as Element of NAT ;
x in dom (Start-At ((IC p) + k),SCM ) by A2, XBOOLE_0:def 4;
then x in {(IC SCM )} by FUNCOP_1:19;
then x = IC SCM by TARSKI:def 1;
hence contradiction by AMI_1:48; :: thesis: verum

end;

reconsider SC = IncAddr (Shift (ProgramPart p),k),k as Function ;
reconsider SA = (Start-At ((IC p) + k),SCM ) | NAT as Function ;
A3: ( dom (IncAddr (Shift (ProgramPart p),k),k) c= NAT & dom (DataPart p) c= SCM-Data-Loc ) by AMI_3:72, RELAT_1:def 18;
reconsider SB = (SC +* (DataPart p)) | NAT as Function ;
thus ProgramPart (Relocated p,k) = ((Start-At ((IC p) + k),SCM ) +* ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p))) | NAT by FUNCT_4:15
.= SA +* SB by FUNCT_4:75
.= ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) | NAT by A1, FUNCT_4:21
.= IncAddr (Shift (ProgramPart p),k),k by A3, AMI_2:29, FUNCT_4:81 ; :: thesis: verum