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