let k be natural number ; :: thesis: for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N
for g being FinPartState of S holds DataPart (Relocated g,k) = DataPart g
let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of 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 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,S),S) | (the carrier of S \ ({(IC S)} \/ NAT ));
consider x being Element of dom ((Start-At ((IC g) + k,S),S) | (the carrier of S \ ({(IC S)} \/ NAT )));

A1: now

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

end;

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