theorem :: COMPOS_1:42

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