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
(fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((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 (fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((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: (fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((cos ((2 * x) + h)) - (cos h)))
f . (x + h) = 1 / (sin (x + h)) by A1;
then (fD (f,h)) . x = (1 / (sin (x + h))) - (f . x) by DIFF_1:3
.= (1 / (sin (x + h))) - (1 / (sin x)) by A1
.= ((1 * (sin x)) - (1 * (sin (x + h)))) / ((sin (x + h)) * (sin x)) by A2, XCMPLX_1:130
.= ((sin x) - (sin (x + h))) / (- ((1 / 2) * ((cos ((x + h) + x)) - (cos ((x + h) - x))))) by SIN_COS4:29
.= ((sin x) - (sin (x + h))) / ((- (1 / 2)) * ((cos ((x + h) + x)) - (cos ((x + h) - x))))
.= (((sin x) - (sin (x + h))) / (- (1 / 2))) / ((cos ((2 * x) + h)) - (cos h)) by XCMPLX_1:78
.= (- 2) * (((sin x) - (sin (x + h))) / ((cos ((2 * x) + h)) - (cos h))) ;
hence (fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((cos ((2 * x) + h)) - (cos h))) ; :: thesis: verum