let a, b be real number ; :: thesis: ( b > 0 implies ( geo-seq (a,b) is convergent & lim (geo-seq (a,b)) = 0 ) )
assume A1: b > 0 ; :: 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 A1, SEQ_4:31; :: thesis: verum