let p be FinPartState of SCM+FSA ; :: 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)) | NAT ;
consider x being Element of dom ((Start-At ((IC p) + k)) | NAT );

now

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

end;

then A2: (Start-At ((IC p) + k)) | NAT = {} ;
A3: dom (IncAddr [(Shift (ProgramPart p),k)],k) c= NAT by RELAT_1:def 18;
A4: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;
reconsider kk = (Start-At ((IC p) + k)) | NAT as Function ;
reconsider rr = ((IncAddr [(Shift (ProgramPart p),k)],k) +* (DataPart p)) | NAT as Function ;
thus ProgramPart (Relocated p,k) = ((Start-At ((IC p) + k)) +* ((IncAddr [(Shift (ProgramPart p),k)],k) +* (DataPart p))) | NAT by FUNCT_4:15
.= kk +* rr by FUNCT_4:75
.= ((IncAddr [(Shift (ProgramPart p),k)],k) +* (DataPart p)) | NAT by A2, FUNCT_4:21
.= IncAddr [(Shift (ProgramPart p),k)],k by A3, A4, Lm1, FUNCT_4:81 ; :: thesis: verum