let b, d be Real; :: thesis: for a being non zero Real holds lim (rseq (a,b,a,d)) = 1
let a be non zero Real; :: thesis: lim (rseq (a,b,a,d)) = 1
thus lim (rseq (a,b,a,d)) = a / a by Th11
.= 1 by XCMPLX_1:60 ; :: thesis: verum