theorem :: COMPOS_1:46

for il being Nat
for S being COM-Struct
for k being Nat
for P being preProgram of S holds
( il in dom P iff il + k in dom (Reloc (P,k)) )