let p be FinPartState of SCM+FSA ; :: thesis: for k, l being Element of NAT holds
( l in dom p iff l + k in dom (Relocated p,k) )
let k, l be Element of NAT ; :: thesis: ( l in dom p iff l + k in dom (Relocated p,k) )
reconsider m = l as Element of NAT ;
A1: 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 A2: 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 m in dom (ProgramPart p) by AMI_1:106;
then l + k in dom (ProgramPart (Relocated p,k)) by A1;
hence l + k in dom (Relocated p,k) by A2; :: 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 A3: ex j being Element of NAT st
( l + k = j + k & j in dom (ProgramPart p) ) by A1;
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 A3; :: thesis: verum