theorem LemmaDiffConst: :: NUMBER06:5

for f being Arithmetic_Progression
for i being Nat holds (f . (i + 1)) - (f . i) = (f . 1) - (f . 0)