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