let h, x be Real; ( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) implies (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h))))) )
set f = cosec (#) sec;
assume A1:
( x + (h / 2) in (dom cosec) /\ (dom sec) & x - (h / 2) in (dom cosec) /\ (dom sec) )
; (cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
A2:
( x + (h / 2) in dom cosec & x + (h / 2) in dom sec )
by A1, XBOOLE_0:def 4;
A3:
( x - (h / 2) in dom cosec & x - (h / 2) in dom sec )
by A1, XBOOLE_0:def 4;
A4:
( sin . (x + (h / 2)) <> 0 & cos . (x + (h / 2)) <> 0 )
by A2, RFUNCT_1:3;
A5:
( sin . (x - (h / 2)) <> 0 & cos . (x - (h / 2)) <> 0 )
by A3, RFUNCT_1:3;
( x + (h / 2) in dom (cosec (#) sec) & x - (h / 2) in dom (cosec (#) sec) )
by A1, VALUED_1:def 4;
then (cD ((cosec (#) sec),h)) . x =
((cosec (#) sec) . (x + (h / 2))) - ((cosec (#) sec) . (x - (h / 2)))
by DIFF_1:39
.=
((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec (#) sec) . (x - (h / 2)))
by VALUED_1:5
.=
((cosec . (x + (h / 2))) * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2))))
by VALUED_1:5
.=
(((sin . (x + (h / 2))) ") * (sec . (x + (h / 2)))) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2))))
by A2, RFUNCT_1:def 2
.=
(((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - ((cosec . (x - (h / 2))) * (sec . (x - (h / 2))))
by A2, RFUNCT_1:def 2
.=
(((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * (sec . (x - (h / 2))))
by A3, RFUNCT_1:def 2
.=
(((sin . (x + (h / 2))) ") * ((cos . (x + (h / 2))) ")) - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))
by A3, RFUNCT_1:def 2
.=
(((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) ") - (((sin . (x - (h / 2))) ") * ((cos . (x - (h / 2))) "))
by XCMPLX_1:204
.=
(1 / ((sin . (x + (h / 2))) * (cos . (x + (h / 2))))) - (1 / ((sin . (x - (h / 2))) * (cos . (x - (h / 2)))))
by XCMPLX_1:204
.=
((1 * ((sin . (x - (h / 2))) * (cos . (x - (h / 2))))) - (1 * ((sin . (x + (h / 2))) * (cos . (x + (h / 2)))))) / (((sin . (x + (h / 2))) * (cos . (x + (h / 2)))) * ((sin . (x - (h / 2))) * (cos . (x - (h / 2)))))
by A4, A5, XCMPLX_1:130
.=
((cos ((x - (h / 2)) + (x + (h / 2)))) * (sin ((x - (h / 2)) - (x + (h / 2))))) / (((sin (x + (h / 2))) * (cos (x + (h / 2)))) * ((sin (x - (h / 2))) * (cos (x - (h / 2)))))
by SIN_COS4:40
.=
((cos (2 * x)) * (sin (- h))) / (((1 * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((1 * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))
.=
((cos (2 * x)) * (- (sin h))) / (((((1 / 2) * 2) * (sin (x + (h / 2)))) * (cos (x + (h / 2)))) * ((((1 / 2) * 2) * (sin (x - (h / 2)))) * (cos (x - (h / 2)))))
by SIN_COS:31
.=
(- ((cos (2 * x)) * (sin h))) / (((1 / 2) * ((2 * (sin (x + (h / 2)))) * (cos (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2))))))
.=
(- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * ((2 * (sin (x - (h / 2)))) * (cos (x - (h / 2))))))
by SIN_COS5:5
.=
(- ((cos (2 * x)) * (sin h))) / (((1 / 2) * (sin (2 * (x + (h / 2))))) * ((1 / 2) * (sin (2 * (x - (h / 2))))))
by SIN_COS5:5
.=
- (((cos (2 * x)) * (sin h)) / (((sin ((2 * x) + h)) * (sin ((2 * x) - h))) * (1 / 4)))
.=
- ((1 / (1 / 4)) * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
by XCMPLX_1:103
.=
- (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
;
hence
(cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
; verum