set f = ArProg (a,r);
AA: dom (ArProg (a,r)) = NAT by FUNCT_2:def 1;
for x being object st x in dom (ArProg (a,r)) holds
(ArProg (a,r)) . x is integer

proof

let x be object ; :: thesis: ( x in dom (ArProg (a,r)) implies (ArProg (a,r)) . x is integer )
assume x in dom (ArProg (a,r)) ; :: thesis: (ArProg (a,r)) . x is integer
then reconsider i = x as Nat by AA;
defpred S₁[ Nat] means (ArProg (a,r)) . a is integer ;
B1: S₁[ 0 ] by ArDefRec;
B2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume C1: S₁[k] ; :: thesis: S₁[k + 1]
(ArProg (a,r)) . (k + 1) = ((ArProg (a,r)) . k) + r by ArDefRec;
hence S₁[k + 1] by C1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(B1, B2);
then S₁[i] ;
hence (ArProg (a,r)) . x is integer ; :: thesis: verum

end;

hence ArProg (a,r) is integer-valued by VALUED_0:def 11; :: thesis: verum