theorem Th25: :: COMPOS_1:41
for n being Nat
for S being COM-Struct
for p, q being NAT -defined the InstructionsF of b2 -valued finite Function holds IncAddr ((p +* q),n) = (IncAddr (p,n)) +* (IncAddr (q,n))