for a, b being Real holds
( geo-seq (a,b) is convergent & lim (geo-seq (a,b)) = 0 )