let N be non empty with_non-empty_elements set ; :: thesis: for il being Element of NAT
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent COM-Struct of N
for k being Element of NAT
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
let il be Element of NAT ; :: 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 k being Element of NAT
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,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 k being Element of NAT
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
let k be Element of NAT ; :: thesis: for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )
let P be preProgram of S; :: thesis: ( il in dom P iff il + k in dom (Reloc (P,k)) )
A1: dom (Reloc (P,k)) = { (j + k) where j is Element of NAT : j in dom P } by Th117;
hence ( il in dom P implies il + k in dom (Reloc (P,k)) ) ; :: thesis: ( il + k in dom (Reloc (P,k)) implies il in dom P )
assume il + k in dom (Reloc (P,k)) ; :: thesis: il in dom P
then ex j being Element of NAT st
( il + k = j + k & j in dom P ) by A1;
hence il in dom P ; :: thesis: verum