let f be Arithmetic_Progression; :: thesis: ( ( for i being Nat holds f . i is Prime ) implies difference f is Integer )
assume for i being Nat holds f . i is Prime ; :: thesis: difference f is Integer
then A2: ( f . 0 is Prime & f . 1 is Prime ) ;
difference f = (f . 1) - (f . 0) by NUMBER06:def 5;
hence difference f is Integer by A2; :: thesis: verum