theorem LemmaIntProg: :: NUMBER06:8

for f being Arithmetic_Progression st ex i being Nat st
( f . i is Integer & difference f is Integer ) holds
f is integer-valued