let k be natural number ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N
for g being FinPartState of S st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
let S be non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of NAT ,N; :: thesis: for g being FinPartState of S st S is realistic holds
ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
let g be FinPartState of S; :: thesis: ( S is realistic implies ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k )
assume A1: S is realistic ; :: thesis: ProgramPart (Relocated g,k) = IncAddr (Shift (ProgramPart g),k),k
set I = NAT ;
set B = the carrier of S \ ({(IC S)} \/ NAT );
set X = (Start-At ((IC g) + k)) | NAT ;
set f = IncAddr (Shift (ProgramPart g),k),k;
consider x being Element of dom ((Start-At ((IC g) + k)) | NAT );

now

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

end;

then (Start-At ((IC g) + k)) | NAT is Relation of {} ,{} by RELSET_1:25;
then A3: (Start-At ((IC g) + k)) | NAT = {} ;
A4: dom (IncAddr (Shift (ProgramPart g),k),k) c= NAT by RELAT_1:def 18;
A5: dom (DataPart g) c= the carrier of S \ ({(IC S)} \/ NAT ) by RELAT_1:87;
A6: NAT misses the carrier of S \ ({(IC S)} \/ NAT ) by Lm3;
thus ProgramPart (Relocated g,k) = ((Start-At ((IC g) + k)) +* ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g))) | NAT by FUNCT_4:15
.= ((Start-At ((IC g) + k)) | NAT ) +* (((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) | NAT ) by FUNCT_4:75
.= ((IncAddr (Shift (ProgramPart g),k),k) +* (DataPart g)) | NAT by A3, FUNCT_4:21
.= IncAddr (Shift (ProgramPart g),k),k by A4, A5, A6, FUNCT_4:81 ; :: thesis: verum