:: deftheorem Def15 defines geo-seq NUMPOLY1:def 15 :
for a, b being Real
for b₃ being Real_Sequence holds
( b₃ = geo-seq (a,b) iff for n being Nat holds b₃ . n = a / (n + b) );