theorem :: COMPOS_1:43

for S being COM-Struct
for p being NAT -defined the InstructionsF of b₁ -valued finite Function
for m, n being Nat holds Reloc ((Reloc (p,m)),n) = Reloc (p,(m + n))