let r be Real; SEQ_2:def 3 ex b1 being set st r <= (rseq (a,b,0,d)) . b1
A1:
(r * d) / d = r
by XCMPLX_1:89;
A2:
(((d * r) - b) / a) * a = (d * r) - b
by XCMPLX_1:87;
consider n being Nat such that
A3:
n > ((d * r) - b) / a
by SEQ_4:3;
take
n
; r <= (rseq (a,b,0,d)) . n
A4:
(rseq (a,b,0,d)) . n = ((a * n) + b) / ((0 * n) + d)
by Th5;
a * n <= (a * ((d * r) - b)) / a
by A2, A3, XREAL_1:65;
then
(a * n) + b <= ((d * r) - b) + b
by A2, XREAL_1:6;
hence
r <= (rseq (a,b,0,d)) . n
by A1, A4, XREAL_1:73; verum