let f be Arithmetic_Progression; :: thesis: ( ex i being Nat st
( f . i is Integer & difference f is Integer ) implies f is integer-valued )
assume ex i being Nat st
( f . i is Integer & difference f is Integer ) ; :: thesis: f is integer-valued
then consider i being Nat such that
A1: ( f . i is Integer & difference f is Integer ) ;
defpred S₁[ Nat] means f . $1 is integer ;
A2: ex k being Nat st S₁[k] by A1;
A3: for k being Nat st k <> 0 & S₁[k] holds
ex n being Nat st
( n < k & S₁[n] )

proof

let k be Nat; :: thesis: ( k <> 0 & S₁[k] implies ex n being Nat st
( n < k & S₁[n] ) )
assume BB: ( k <> 0 & S₁[k] ) ; :: thesis: ex n being Nat st
( n < k & S₁[n] )
then difference f = (f . ((k - 1) + 1)) - (f . (k - 1)) by LemmaDiffConst;
then b1: f . (k - 1) = (f . k) - (difference f) ;
reconsider n = k - 1 as Nat by BB;
take n ; :: thesis: ( n < k & S₁[n] )
thus ( n < k & S₁[n] ) by b1, XREAL_1:44, BB, A1; :: thesis: verum

end;

z1: S₁[ 0 ] from NAT_1:sch 7(A2, A3);
for n being object st n in dom f holds
f . n is integer

proof

let n be object ; :: thesis: ( n in dom f implies f . n is integer )
SS: dom f = NAT by FUNCT_2:def 1;
assume n in dom f ; :: thesis: f . n is integer
then reconsider nn = n as Nat by SS;
f = ArProg ((f . 0),(difference f)) by APAsArProg;
hence f . n is integer by A1, z1; :: thesis: verum

end;

hence f is integer-valued by VALUED_0:def 11; :: thesis: verum