theorem Th25: :: AMI_6:25

for a being Data-Location
for i1, k being Nat holds IncAddr ((a >0_goto i1),k) = a >0_goto (i1 + k)