let p be FinPartState of SCM ; :: thesis: for k being Element of NAT holds IC SCM in dom (Relocated p,k)
let k be Element of NAT ; :: thesis: IC SCM in dom (Relocated p,k)
dom (Start-At ((IC p) + k),SCM ) = {(IC SCM )} by FUNCOP_1:19;
then ( Relocated p,k = (Start-At ((IC p) + k),SCM ) +* ((IncAddr (Shift (ProgramPart p),k),k) +* (DataPart p)) & IC SCM in dom (Start-At ((IC p) + k),SCM ) ) by FUNCT_4:15, TARSKI:def 1;
hence IC SCM in dom (Relocated p,k) by FUNCT_4:13; :: thesis: verum