theorem Th41: :: SCMFSA10:41

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