let m be Nat; :: thesis: rng (x_r-seq m) c= ].0,(PI / 2).[
set f = x_r-seq m;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (x_r-seq m) or y in ].0,(PI / 2).[ )
assume y in rng (x_r-seq m) ; :: thesis: y in ].0,(PI / 2).[
then consider n being Nat such that
A1: 1 <= n and
A2: n <= len (x_r-seq m) and
A3: y = (x_r-seq m) . n by Lm2;
A4: len (x_r-seq m) = m by Th19;
then A5: (x_r-seq m) . n = (n * PI) / ((2 * m) + 1) by A1, A2, Th19;
2 * n <= 2 * m by A2, A4, XREAL_1:64;
then (2 * n) + 1 <= (2 * m) + 1 by XREAL_1:6;
then A6: (n * PI) / ((2 * n) + 1) >= (n * PI) / ((2 * m) + 1) by XREAL_1:118;
A7: (((2 * n) + 1) * (n ")) " = (((2 * n) + 1) ") * ((n ") ") by XCMPLX_1:204;
A8: (2 * n) / n = 2 by A1, XCMPLX_1:89;
2 + (1 / n) > 2 + 0 by A1, XREAL_1:8;
then (((2 * n) + 1) * (n ")) " < (2 * (1 ")) " by A8, XREAL_1:88;
then PI * (n / ((2 * n) + 1)) < PI * (1 / 2) by A7, XREAL_1:68;
then (n * PI) / ((2 * m) + 1) < PI / 2 by A6, XXREAL_0:2;
hence y in ].0,(PI / 2).[ by A1, A3, A5, XXREAL_1:4; :: thesis: verum