theorem :: COMPOS_1:43
for S being COM-Struct
for p being NAT -defined the InstructionsF of b1 -valued finite Function
for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))