let m be Nat; sqr (cosec (x_r-seq m)) = 1 + (sqr (cot (x_r-seq m)))
set f = x_r-seq m;
A1:
len (sqr (cosec (x_r-seq m))) = len (cosec (x_r-seq m))
by CARD_1:def 7;
A2:
len (cosec (x_r-seq m)) = len (x_r-seq m)
by CARD_1:def 7;
A3:
len (x_r-seq m) = m
by Th19;
A4:
len (1 + (sqr (cot (x_r-seq m)))) = len (sqr (cot (x_r-seq m)))
by CARD_1:def 7;
A5:
len (sqr (cot (x_r-seq m))) = len (cot (x_r-seq m))
by CARD_1:def 7;
A6:
len (cot (x_r-seq m)) = len (x_r-seq m)
by CARD_1:def 7;
thus
len (sqr (cosec (x_r-seq m))) = len (1 + (sqr (cot (x_r-seq m))))
by A1, A2, A4, A5, CARD_1:def 7; FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len (sqr (cosec (x_r-seq m))) or (sqr (cosec (x_r-seq m))) . b1 = (1 + (sqr (cot (x_r-seq m)))) . b1 )
let k be Nat; ( not 1 <= k or not k <= len (sqr (cosec (x_r-seq m))) or (sqr (cosec (x_r-seq m))) . k = (1 + (sqr (cot (x_r-seq m)))) . k )
assume that
A7:
1 <= k
and
A8:
k <= len (sqr (cosec (x_r-seq m)))
; (sqr (cosec (x_r-seq m))) . k = (1 + (sqr (cot (x_r-seq m)))) . k
A9:
k in dom (x_r-seq m)
by A1, A2, A7, A8, FINSEQ_3:25;
then A10:
(cosec (x_r-seq m)) . k = cosec ((x_r-seq m) . k)
by Def4;
A11:
(sqr (cot (x_r-seq m))) . k = ((cot (x_r-seq m)) . k) ^2
by VALUED_1:11;
A12:
(cot (x_r-seq m)) . k = cot ((x_r-seq m) . k)
by A9, Def3;
A13:
0 < (x_r-seq m) . k
by A1, A2, A3, A7, A8, Th21;
A14:
(x_r-seq m) . k < PI / 2
by A1, A2, A3, A7, A8, Th21;
PI / 2 < PI / 1
by XREAL_1:76;
then
(x_r-seq m) . k < PI
by A14, XXREAL_0:2;
then
(x_r-seq m) . k in ].0,PI.[
by A13, XXREAL_1:4;
then
sin ((x_r-seq m) . k) <> 0
by COMPTRIG:7;
then A15:
(cosec ((x_r-seq m) . k)) ^2 = 1 + ((cot ((x_r-seq m) . k)) ^2)
by SIN_COS5:14;
k in dom (1 + (sqr (cot (x_r-seq m))))
by A1, A2, A4, A5, A6, A7, A8, FINSEQ_3:25;
hence (1 + (sqr (cot (x_r-seq m)))) . k =
((cosec (x_r-seq m)) . k) ^2
by A10, A11, A12, A15, VALUED_1:def 2
.=
(sqr (cosec (x_r-seq m))) . k
by VALUED_1:11
;
verum