let x0, x1 be Real; ( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) implies [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1) )
assume A1:
( x0 in (dom cosec) /\ (dom sec) & x1 in (dom cosec) /\ (dom sec) )
; [!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1)
A2:
( x0 in dom cosec & x0 in dom sec )
by A1, XBOOLE_0:def 4;
A3:
( x1 in dom cosec & x1 in dom sec )
by A1, XBOOLE_0:def 4;
A4:
( sin . x0 <> 0 & cos . x0 <> 0 )
by A2, RFUNCT_1:3;
A5:
( sin . x1 <> 0 & cos . x1 <> 0 )
by A3, RFUNCT_1:3;
[!(cosec (#) sec),x0,x1!] =
(((cosec . x0) * (sec . x0)) - ((cosec (#) sec) . x1)) / (x0 - x1)
by VALUED_1:5
.=
(((cosec . x0) * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1)
by VALUED_1:5
.=
((((sin . x0) ") * (sec . x0)) - ((cosec . x1) * (sec . x1))) / (x0 - x1)
by A2, RFUNCT_1:def 2
.=
((((sin . x0) ") * ((cos . x0) ")) - ((cosec . x1) * (sec . x1))) / (x0 - x1)
by A2, RFUNCT_1:def 2
.=
((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * (sec . x1))) / (x0 - x1)
by A3, RFUNCT_1:def 2
.=
((((sin . x0) ") * ((cos . x0) ")) - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1)
by A3, RFUNCT_1:def 2
.=
((((sin . x0) * (cos . x0)) ") - (((sin . x1) ") * ((cos . x1) "))) / (x0 - x1)
by XCMPLX_1:204
.=
((1 / ((sin . x0) * (cos . x0))) - (1 / ((sin . x1) * (cos . x1)))) / (x0 - x1)
by XCMPLX_1:204
.=
(((1 * ((sin . x1) * (cos . x1))) - (1 * ((sin . x0) * (cos . x0)))) / (((sin . x0) * (cos . x0)) * ((sin . x1) * (cos . x1)))) / (x0 - x1)
by A4, A5, XCMPLX_1:130
.=
(((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * ((2 * (sin x0)) * (cos x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1)
by SIN_COS4:40
.=
(((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * ((2 * (sin x1)) * (cos x1))))) / (x0 - x1)
by SIN_COS5:5
.=
(((cos (x1 + x0)) * (sin (x1 - x0))) / (((1 / 2) * (sin (2 * x0))) * ((1 / 2) * (sin (2 * x1))))) / (x0 - x1)
by SIN_COS5:5
.=
(((cos (x1 + x0)) * (sin (x1 - x0))) / ((((sin (2 * x0)) * (sin (2 * x1))) * 1) / 4)) / (x0 - x1)
.=
((1 / (1 / 4)) * (((cos (x1 + x0)) * (sin (x1 - x0))) / ((sin (2 * x0)) * (sin (2 * x1))))) / (x0 - x1)
by XCMPLX_1:103
.=
((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1)
;
hence
[!(cosec (#) sec),x0,x1!] = ((4 * ((cos (x1 + x0)) * (sin (x1 - x0)))) / ((sin (2 * x0)) * (sin (2 * x1)))) / (x0 - x1)
; verum