let h, x be Real; for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
let f be Function of REAL,REAL; ( ( for x being Real holds f . x = (cot (#) cos) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2))) )
assume that
A1:
for x being Real holds f . x = (cot (#) cos) . x
and
A2:
( x + (h / 2) in dom cot & x - (h / 2) in dom cot )
; (cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
(cD (f,h)) . x =
(f . (x + (h / 2))) - (f . (x - (h / 2)))
by DIFF_1:5
.=
((cot (#) cos) . (x + (h / 2))) - (f . (x - (h / 2)))
by A1
.=
((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2)))
by A1
.=
((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cot (#) cos) . (x - (h / 2)))
by VALUED_1:5
.=
((cot . (x + (h / 2))) * (cos . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2))))
by VALUED_1:5
.=
(((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cos . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cos . (x - (h / 2))))
by A2, RFUNCT_1:def 1
.=
(((cos (x + (h / 2))) / (sin (x + (h / 2)))) * (cos (x + (h / 2)))) - (((cos (x - (h / 2))) / (sin (x - (h / 2)))) * (cos (x - (h / 2))))
by A2, RFUNCT_1:def 1
.=
((cos (x + (h / 2))) / ((sin (x + (h / 2))) / (cos (x + (h / 2))))) - (((cos (x - (h / 2))) / (sin (x - (h / 2)))) * (cos (x - (h / 2))))
by XCMPLX_1:82
.=
((cos (x + (h / 2))) / ((sin (x + (h / 2))) / (cos (x + (h / 2))))) - ((cos (x - (h / 2))) / ((sin (x - (h / 2))) / (cos (x - (h / 2)))))
by XCMPLX_1:82
.=
(((cos (x + (h / 2))) * (cos (x + (h / 2)))) / (sin (x + (h / 2)))) - ((cos (x - (h / 2))) / ((sin (x - (h / 2))) / (cos (x - (h / 2)))))
by XCMPLX_1:77
.=
(((cos (x + (h / 2))) * (cos (x + (h / 2)))) / (sin (x + (h / 2)))) - (((cos (x - (h / 2))) * (cos (x - (h / 2)))) / (sin (x - (h / 2))))
by XCMPLX_1:77
.=
((1 - ((sin (x + (h / 2))) * (sin (x + (h / 2))))) / (sin (x + (h / 2)))) - (((cos (x - (h / 2))) * (cos (x - (h / 2)))) / (sin (x - (h / 2))))
by SIN_COS4:5
.=
((1 / (sin (x + (h / 2)))) - (((sin (x + (h / 2))) * (sin (x + (h / 2)))) / (sin (x + (h / 2))))) - ((1 - ((sin (x - (h / 2))) * (sin (x - (h / 2))))) / (sin (x - (h / 2))))
by SIN_COS4:5
.=
((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - ((1 / (sin (x - (h / 2)))) - (((sin (x - (h / 2))) * (sin (x - (h / 2)))) / (sin (x - (h / 2)))))
by A2, FDIFF_8:2, XCMPLX_1:89
.=
((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - ((1 / (sin (x - (h / 2)))) - (sin (x - (h / 2))))
by A2, FDIFF_8:2, XCMPLX_1:89
.=
(((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
;
hence
(cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))
; verum