for b, d being Real holds lim (rseq (0,b,0,d)) = b / d