let h, x be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h)))
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = 1 / (sin x) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 implies (cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h))) )
assume that
A1: for x being Real holds f . x = 1 / (sin x) and
A2: ( sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 ) ; :: thesis: (cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h)))
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (1 / (sin (x + (h / 2)))) - (f . (x - (h / 2))) by A1
.= (1 / (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2)))) by A1
.= ((1 * (sin (x - (h / 2)))) - (1 * (sin (x + (h / 2))))) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))) by A2, XCMPLX_1:130
.= ((sin (x - (h / 2))) - (sin (x + (h / 2)))) / (- ((1 / 2) * ((cos ((x + (h / 2)) + (x - (h / 2)))) - (cos ((x + (h / 2)) - (x - (h / 2))))))) by SIN_COS4:29
.= ((sin (x - (h / 2))) - (sin (x + (h / 2)))) / ((- (1 / 2)) * ((cos (2 * x)) - (cos h)))
.= (((sin (x - (h / 2))) - (sin (x + (h / 2)))) / (- (1 / 2))) / ((cos (2 * x)) - (cos h)) by XCMPLX_1:78
.= (- 2) * (((sin (x - (h / 2))) - (sin (x + (h / 2)))) / ((cos (2 * x)) - (cos h))) ;
hence (cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h))) ; :: thesis: verum