theorem Th36: :: SCMRING3:37

for R being Ring
for i1, k being Nat holds IncAddr ((goto (i1,R)),k) = goto ((i1 + k),R)