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