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