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:31; :: thesis: verum

end;

hence ArProg (a,r) is non-decreasing by SEQM_3:def 8; :: thesis: verum