theorem Th11: :: BASEL_1:11

for a, b, d being Real
for c being non zero Real holds lim (rseq (a,b,c,d)) = a / c