let h, x be Real; :: thesis: ( x in dom cosec & x - h in dom cosec implies (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) )
set f = cosec (#) cosec;
assume A1: ( x in dom cosec & x - h in dom cosec ) ; :: thesis: (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))
A2: ( sin . x <> 0 & sin . (x - h) <> 0 ) by A1, RFUNCT_1:3;
( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) )

proof

( x in (dom cosec) /\ (dom cosec) & x - h in (dom cosec) /\ (dom cosec) ) by A1;
hence ( x in dom (cosec (#) cosec) & x - h in dom (cosec (#) cosec) ) by VALUED_1:def 4; :: thesis: verum

end;

then (bD ((cosec (#) cosec),h)) . x = ((cosec (#) cosec) . x) - ((cosec (#) cosec) . (x - h)) by DIFF_1:38
.= ((cosec . x) * (cosec . x)) - ((cosec (#) cosec) . (x - h)) by VALUED_1:5
.= ((cosec . x) * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by VALUED_1:5
.= (((sin . x) ") * (cosec . x)) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def 2
.= (((sin . x) ") * ((sin . x) ")) - ((cosec . (x - h)) * (cosec . (x - h))) by A1, RFUNCT_1:def 2
.= (((sin . x) ") * ((sin . x) ")) - (((sin . (x - h)) ") * (cosec . (x - h))) by A1, RFUNCT_1:def 2
.= (((sin . x) ") ^2) - (((sin . (x - h)) ") ^2) by A1, RFUNCT_1:def 2
.= ((1 / (sin . x)) - (1 / (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h))))
.= (((1 * (sin . (x - h))) - (1 * (sin . x))) / ((sin . x) * (sin . (x - h)))) * ((1 / (sin . x)) + (1 / (sin . (x - h)))) by A2, XCMPLX_1:130
.= (((sin . (x - h)) - (sin . x)) / ((sin . x) * (sin . (x - h)))) * (((sin . (x - h)) + (sin . x)) / ((sin . x) * (sin . (x - h)))) by A2, XCMPLX_1:116
.= (((sin . (x - h)) - (sin . x)) * ((sin . (x - h)) + (sin . x))) / (((sin . x) * (sin . (x - h))) * ((sin . x) * (sin . (x - h)))) by XCMPLX_1:76
.= (((sin (x - h)) * (sin (x - h))) - ((sin x) * (sin x))) / (((sin x) * (sin (x - h))) ^2)
.= ((sin ((x - h) + x)) * (sin ((x - h) - x))) / (((sin x) * (sin (x - h))) ^2) by SIN_COS4:37
.= ((sin ((2 * x) - h)) * (sin (- h))) / ((- ((1 / 2) * ((cos (x + (x - h))) - (cos (x - (x - h)))))) ^2) by SIN_COS4:29
.= ((sin ((2 * x) - h)) * (- (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2)) by SIN_COS:31
.= - ((1 * ((sin ((2 * x) - h)) * (sin h))) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2)))
.= - ((1 / (1 / 4)) * (((sin ((2 * x) - h)) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))) by XCMPLX_1:76
.= - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ;
hence (bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2)) ; :: thesis: verum