let p be FinPartState of SCM+FSA ; :: thesis: for k being Element of NAT
for l being Instruction-Location of SCM+FSA holds
( l in dom p iff l + k in dom (Relocated p,k) )
let k be Element of NAT ; :: thesis: for l being Instruction-Location of SCM+FSA holds
( l in dom p iff l + k in dom (Relocated p,k) )
let l be Instruction-Location of SCM+FSA ; :: thesis: ( l in dom p iff l + k in dom (Relocated p,k) )
reconsider m = l as Element of NAT by ORDINAL1:def 13;
A3: dom (ProgramPart (Relocated p,k)) = { (j + k) where j is Element of NAT : j in dom (ProgramPart p) } by Th3;
ProgramPart (Relocated p,k) c= Relocated p,k by RELAT_1:88;
then A4: dom (ProgramPart (Relocated p,k)) c= dom (Relocated p,k) by GRFUNC_1:8;

hereby :: thesis: ( l + k in dom (Relocated p,k) implies l in dom p )

assume l in dom p ; :: thesis: l + k in dom (Relocated p,k)
then insloc m in dom (ProgramPart p) by AMI_1:106;
then l + k in dom (ProgramPart (Relocated p,k)) by A3;
hence l + k in dom (Relocated p,k) by A4; :: thesis: verum

end;

assume l + k in dom (Relocated p,k) ; :: thesis: l in dom p
then l + k in dom (ProgramPart (Relocated p,k)) by AMI_1:106;
then consider j being Element of NAT such that
A5: l + k = j + k and
A6: j in dom (ProgramPart p) by A3;
ProgramPart p c= p by RELAT_1:88;
then dom (ProgramPart p) c= dom p by GRFUNC_1:8;
hence l in dom p by A5, A6; :: thesis: verum