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

end;

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