let f be Arithmetic_Progression; :: thesis: for i being Nat holds (f . (i + 1)) - (f . i) = (f . 1) - (f . 0)
let i be Nat; :: thesis: (f . (i + 1)) - (f . i) = (f . 1) - (f . 0)
dom f = NAT by FUNCT_2:def 1;
then ( i in dom f & 0 in dom f & 1 in dom f & i + 1 in dom f ) by ORDINAL1:def 12;
then (f . (i + 1)) - (f . i) = (f . (0 + 1)) - (f . 0) by APLikeDef;
hence (f . (i + 1)) - (f . i) = (f . 1) - (f . 0) ; :: thesis: verum