let p be FinPartState of SCM ; :: 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
A2: DataPart (Start-At ((IC p) + k)) = {} by AMI_1:138;
reconsider SA = DataPart (Start-At ((IC p) + k)) as Function ;
reconsider SC = IncAddr (Shift (ProgramPart p),k),k as Function ;
reconsider SB = (SC +* (DataPart p)) | SCM-Data-Loc as Function ;
A3: dom (IncAddr (Shift (ProgramPart p),k),k) c= NAT by RELAT_1:def 18;
A4: dom (DataPart p) c= SCM-Data-Loc by AMI_3:72, RELAT_1:87;
thus DataPart (Relocated p,k) = DataPart ((Start-At ((IC p) + k)) +* ([(IncAddr (Shift (ProgramPart p),k),k)] +* (DataPart p))) by FUNCT_4:15
.= SA +* SB by AMI_3:72, FUNCT_4:75
.= DataPart ([(IncAddr (Shift (ProgramPart p),k),k)] +* (DataPart p)) by A2, AMI_3:72, FUNCT_4:21
.= DataPart p by A3, A4, AMI_2:29, AMI_3:72, FUNCT_4:81 ; :: thesis: verum