set f = ArProg (a,r);
set i = the Nat;
assume ArProg (a,r) is constant ; :: thesis: contradiction
then A2: (ArProg (a,r)) . the Nat = (ArProg (a,r)) . ( the Nat + 1) by VALUED_0:23;
(ArProg (a,r)) . ( the Nat + 1) = ((ArProg (a,r)) . the Nat) + r by ArDefRec;
then r = 0 by A2;
hence contradiction ; :: thesis: verum