theorem :: COMPOS_1:35

for S being COM-Struct
for il being Nat
for g being NAT -defined the InstructionsF of b₁ -valued finite Function
for k being Nat
for I being Instruction of S st il in dom g & I = g . il holds
IncAddr (I,k) = (Reloc (g,k)) . (il + k)