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

proof

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

end;

hence ArProg (a,0) is constant by VALUED_0:25; :: thesis: verum