let m be Nat; :: thesis: Sum (sqr (cot (x_r-seq m))) <= Sum ((sqr (x_r-seq m)) ")
set f = x_r-seq m;
set f1 = sqr (cot (x_r-seq m));
set f2 = (sqr (x_r-seq m)) " ;
A1: len (x_r-seq m) = m by Th19;
A2: len (cot (x_r-seq m)) = len (x_r-seq m) by Lm14;
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 (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . n

let n be Nat; :: thesis: ( n in Seg m implies (sqr (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . n )
assume n in Seg m ; :: thesis: (sqr (cot (x_r-seq m))) . n <= ((sqr (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 (cot (x_r-seq m))) . n = ((cot (x_r-seq m)) . n) ^2 by VALUED_1:11;
A7: (cot (x_r-seq m)) . n = cot ((x_r-seq m) . n) by A5, Def3;
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: (tan ((x_r-seq m) . n)) " = cot ((x_r-seq m) . n) by Th15;
A11: (x_r-seq m) . n < PI / 2 by A4, Th21;
A12: 0 < (x_r-seq m) . n by A4, Th21;
then A13: (x_r-seq m) . n in ].((- (PI / 2)) + (PI * 0)),((PI / 2) + (PI * 0)).[ by A11, XXREAL_1:4;
].((- (PI / 2)) + (PI * 0)),((PI / 2) + (PI * 0)).[ in { ].((- (PI / 2)) + (PI * i)),((PI / 2) + (PI * i)).[ where i is Integer : verum } ;
then (x_r-seq m) . n in dom tan by A13, Th16, TARSKI:def 4;
then tan . ((x_r-seq m) . n) = tan ((x_r-seq m) . n) by RFUNCT_1:def 1;
then A14: ((tan . ((x_r-seq m) . n)) ^2) " = (cot ((x_r-seq m) . n)) ^2 by A10, XCMPLX_1:204;
(x_r-seq m) . n <= tan . ((x_r-seq m) . n) by A4, A12, Th18, Th21;
then ((x_r-seq m) . n) ^2 <= (tan . ((x_r-seq m) . n)) ^2 by A12, XREAL_1:66;
hence (sqr (cot (x_r-seq m))) . n <= ((sqr (x_r-seq m)) ") . n by A6, A7, A8, A9, A12, A14, XREAL_1:85; :: thesis: verum

end;

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