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 homogeneous regular J/A-independent COM-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 homogeneous regular J/A-independent COM-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, Th16;
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 Th16;
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