theorem ArDefNth: :: NUMBER06:7

for a, r being Real
for i being Nat holds (ArProg (a,r)) . i = a + (i * r)