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