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