:: deftheorem Def1 defines aseq IRRAT_1:def 1 :
for k being Nat
for b₂ being Real_Sequence holds
( b₂ = aseq k iff for n being Nat holds b₂ . n = (n - k) / n );