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

proof

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

end;

hence ArProg (a,r) is AP-like ; :: thesis: verum