let r be Real; :: according to SEQ_2:def 3 :: thesis: ex b₁ being set st r <= (rseq (a,b,0,d)) . b₁
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 ; :: thesis: 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:64;
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:72; :: thesis: verum