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 holds DataPart (Relocated g,k) = DataPart g
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 holds DataPart (Relocated g,k) = DataPart g
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 holds DataPart (Relocated g,k) = DataPart g
let g be FinPartState of S; :: thesis: DataPart (Relocated g,k) = DataPart g
set I = NAT ;
set B = the carrier of S \ ({(IC S)} \/ NAT );
set X = (Start-At ((IC g) + k)) | (the carrier of S \ ({(IC S)} \/ NAT ));
consider x being Element of dom ((Start-At ((IC g) + k)) | (the carrier of S \ ({(IC S)} \/ NAT )));

now

assume (Start-At ((IC g) + k)) | (the carrier of S \ ({(IC S)} \/ NAT )) <> {} ; :: thesis: contradiction
then dom ((Start-At ((IC g) + k)) | (the carrier of S \ ({(IC S)} \/ NAT ))) <> {} ;
then x in dom ((Start-At ((IC g) + k)) | (the carrier of S \ ({(IC S)} \/ NAT ))) ;
then A1: x in (dom (Start-At ((IC g) + k))) /\ (the carrier of S \ ({(IC S)} \/ NAT )) by RELAT_1:90;
then x in the carrier of S \ ({(IC S)} \/ NAT ) by XBOOLE_0:def 4;
then A2: not x in {(IC S)} \/ NAT by XBOOLE_0:def 5;
x in dom (Start-At ((IC g) + k)) by A1, XBOOLE_0:def 4;
then x in {(IC S)} by FUNCOP_1:19;
hence contradiction by A2, XBOOLE_0:def 3; :: thesis: verum

end;

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