theorem Th21: :: COMPOS_1:33

for S being COM-Struct
for k being Nat
for p being NAT -defined the InstructionsF of b₁ -valued finite Function holds dom (Reloc (p,k)) = { (j + k) where j is Nat : j in dom p }