let m be Nat; :: thesis: Sum (sqr (cosec (x_r-seq m))) = ((2 * m) * ((2 * m) + 2)) / 6
set f = x_r-seq m;
A1: len (sqr (cot (x_r-seq m))) = len (cot (x_r-seq m)) by CARD_1:def 7
.= len (x_r-seq m) by CARD_1:def 7
.= m by BASEL_1:21 ;
A2: Sum (1 + (sqr (cot (x_r-seq m)))) = (1 * (len (sqr (cot (x_r-seq m))))) + (Sum (sqr (cot (x_r-seq m)))) by BASEL_1:4;
Sum (sqr (cot (x_r-seq m))) = ((2 * m) * ((2 * m) - 1)) / 6 by Th28;
hence Sum (sqr (cosec (x_r-seq m))) = ((2 * m) * ((2 * m) + 2)) / 6 by A1, A2, BASEL_1:26; :: thesis: verum