let p be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT holds DataPart (Relocated p,k) = DataPart p
let k be Element of NAT ; :: thesis: DataPart (Relocated p,k) = DataPart p
A1: DataPart (Start-At ((IC p) + k),SCM+FSA ) = {} by AMI_1:138;
reconsider kk = DataPart (Start-At ((IC p) + k),SCM+FSA ) as Function ;
A2: dom (IncAddr (Shift (ProgramPart p),k),k) c= NAT by RELAT_1:def 18;
reconsider rr = DataPart ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) as Function ;
A3: dom (DataPart p) c= Int-Locations \/ FinSeq-Locations by RELAT_1:87, SCMFSA_2:127;
thus DataPart (Relocated p,k) = DataPart ((Start-At ((IC p) + k),SCM+FSA ) +* ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p))) by FUNCT_4:15
.= kk +* rr by FUNCT_4:75
.= DataPart ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) by A1, FUNCT_4:21
.= DataPart p by A2, A3, Lm1, FUNCT_4:81, SCMFSA_2:127 ; :: thesis: verum