let a, b be Real; :: thesis: ( geo-seq (a,b) is convergent & lim (geo-seq (a,b)) = 0 )
for k being Nat holds (geo-seq (a,b)) . k = a / (k + b) by Def15;
hence ( geo-seq (a,b) is convergent & lim (geo-seq (a,b)) = 0 ) by SEQ_4:31; :: thesis: verum