let b, d be Real; :: thesis: lim (rseq (0,b,0,d)) = b / d
thus lim (rseq (0,b,0,d)) = (rseq (0,b,0,d)) . 0 by SEQ_4:26
.= b / d by Th6 ; :: thesis: verum