set f = ArProg (a,r);
for i being Nat holds (ArProg (a,r)) . i < (ArProg (a,r)) . (i + 1)

proof

let i be Nat; :: thesis: (ArProg (a,r)) . i < (ArProg (a,r)) . (i + 1)
(ArProg (a,r)) . (i + 1) = ((ArProg (a,r)) . i) + r by ArDefRec;
hence (ArProg (a,r)) . i < (ArProg (a,r)) . (i + 1) by XREAL_1:29; :: thesis: verum

end;

hence ArProg (a,r) is increasing by SEQM_3:def 6; :: thesis: verum