:: deftheorem ArDefRec defines ArProg NUMBER06:def 4 :
for a, r being Real
for b₃ being sequence of REAL holds
( b₃ = ArProg (a,r) iff ( b₃ . 0 = a & ( for i being Nat holds b₃ . (i + 1) = (b₃ . i) + r ) ) );