let m be Nat; :: thesis: Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m)))
set f = x_r-seq m;
set f1 = sqr (cosec (x_r-seq m));
set f2 = (sqr (x_r-seq m)) " ;
A1: len (x_r-seq m) = m by Th19;
A2: len (cosec (x_r-seq m)) = len (x_r-seq m) by Lm15;
A3: len (sqr (x_r-seq m)) = len (x_r-seq m) by RVSUM_1:143;

now :: thesis: for n being Nat st n in Seg m holds
((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n

let n be Nat; :: thesis: ( n in Seg m implies ((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n )
assume n in Seg m ; :: thesis: ((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n
then A4: ( 1 <= n & n <= m ) by FINSEQ_1:1;
then A5: n in dom (x_r-seq m) by A1, FINSEQ_3:25;
A6: (sqr (cosec (x_r-seq m))) . n = ((cosec (x_r-seq m)) . n) ^2 by VALUED_1:11;
A7: (cosec (x_r-seq m)) . n = cosec ((x_r-seq m) . n) by A5, Def4;
A8: ((sqr (x_r-seq m)) ") . n = ((sqr (x_r-seq m)) . n) " by VALUED_1:10;
A9: (sqr (x_r-seq m)) . n = ((x_r-seq m) . n) ^2 by VALUED_1:11;
A10: (x_r-seq m) . n < PI / 2 by A4, Th21;
A11: 0 < (x_r-seq m) . n by A4, Th21;
A12: ((sin . ((x_r-seq m) . n)) ^2) " = (cosec ((x_r-seq m) . n)) ^2 by XCMPLX_1:204;
PI / 2 < PI / 1 by XREAL_1:76;
then (x_r-seq m) . n < PI by A10, XXREAL_0:2;
then (x_r-seq m) . n in ].0,PI.[ by A11, XXREAL_1:4;
then A13: 0 < sin ((x_r-seq m) . n) by COMPTRIG:7;
sin . ((x_r-seq m) . n) <= (x_r-seq m) . n by A11, Th17;
then (sin . ((x_r-seq m) . n)) ^2 <= ((x_r-seq m) . n) ^2 by A13, XREAL_1:66;
hence ((sqr (x_r-seq m)) ") . n <= (sqr (cosec (x_r-seq m))) . n by A6, A7, A8, A9, A12, A13, XREAL_1:85; :: thesis: verum

end;

hence Sum ((sqr (x_r-seq m)) ") <= Sum (sqr (cosec (x_r-seq m))) by A1, A2, A3, RVSUM_1:82; :: thesis: verum