let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for g being FinPartState of S
for il, k being Element of NAT holds
( il in dom g iff il + k in dom (Relocated g,k) )
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for g being FinPartState of S
for il, k being Element of NAT holds
( il in dom g iff il + k in dom (Relocated g,k) )
let g be FinPartState of S; :: thesis: for il, k being Element of NAT holds
( il in dom g iff il + k in dom (Relocated g,k) )
let il, k be Element of NAT ; :: thesis: ( il in dom g iff il + k in dom (Relocated g,k) )
consider m being natural number such that
A2: il = m ;
A4: dom (ProgramPart (Relocated g,k)) = dom (Reloc (ProgramPart g),k) by Th69
.= { (j + k) where j is Element of NAT : j in dom (ProgramPart g) } by Th70 ;
ProgramPart (Relocated g,k) c= Relocated g,k by RELAT_1:88;
then A5: dom (ProgramPart (Relocated g,k)) c= dom (Relocated g,k) by GRFUNC_1:8;

hereby :: thesis: ( il + k in dom (Relocated g,k) implies il in dom g )

assume il in dom g ; :: thesis: il + k in dom (Relocated g,k)
then m in dom (ProgramPart g) by A2, COMPOS_1:16;
then il + k in dom (ProgramPart (Relocated g,k)) by A2, A4;
hence il + k in dom (Relocated g,k) by A5; :: thesis: verum

end;

assume il + k in dom (Relocated g,k) ; :: thesis: il in dom g
then il + k in dom (ProgramPart (Relocated g,k)) by COMPOS_1:16;
then consider j being Element of NAT such that
A7: il + k = j + k and
A8: j in dom (ProgramPart g) by A4;
ProgramPart g c= g by RELAT_1:88;
then dom (ProgramPart g) c= dom g by GRFUNC_1:8;
hence il in dom g by A8, A7; :: thesis: verum