theorem Th8: :: COMPOS_1:17

for k, m being Nat
for S being COM-Struct
for F being preProgram of S holds IncAddr ((IncAddr (F,k)),m) = IncAddr (F,(k + m))