let x, h 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
(fD f,h) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x)
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 (fD f,h) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x) )
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: (fD f,h) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x)
(fD f,h) . x = (f . (x + h)) - (f . x) by DIFF_1:3
.= ((cot (#) cos ) . (x + h)) - (f . x) by A1
.= ((cot (#) cos ) . (x + h)) - ((cot (#) cos ) . x) by A1
.= ((cot . (x + h)) * (cos . (x + h))) - ((cot (#) cos ) . x) by VALUED_1:5
.= ((cot . (x + h)) * (cos . (x + h))) - ((cot . x) * (cos . x)) by VALUED_1:5
.= (((cos . (x + h)) * ((sin . (x + h)) " )) * (cos . (x + h))) - ((cot . x) * (cos . x)) by A2, RFUNCT_1:def 4
.= (((cos (x + h)) / (sin (x + h))) * (cos (x + h))) - (((cos x) / (sin x)) * (cos x)) by A2, RFUNCT_1:def 4
.= ((cos (x + h)) / ((sin (x + h)) / (cos (x + h)))) - (((cos x) / (sin x)) * (cos x)) by XCMPLX_1:83
.= ((cos (x + h)) / ((sin (x + h)) / (cos (x + h)))) - ((cos x) / ((sin x) / (cos x))) by XCMPLX_1:83
.= (((cos (x + h)) * (cos (x + h))) / (sin (x + h))) - ((cos x) / ((sin x) / (cos x))) by XCMPLX_1:78
.= (((cos (x + h)) * (cos (x + h))) / (sin (x + h))) - (((cos x) * (cos x)) / (sin x)) by XCMPLX_1:78
.= ((1 - ((sin (x + h)) * (sin (x + h)))) / (sin (x + h))) - (((cos x) * (cos x)) / (sin x)) by SIN_COS4:7
.= ((1 / (sin (x + h))) - (((sin (x + h)) * (sin (x + h))) / (sin (x + h)))) - ((1 - ((sin x) * (sin x))) / (sin x)) by SIN_COS4:7
.= ((1 / (sin (x + h))) - (sin (x + h))) - ((1 / (sin x)) - (((sin x) * (sin x)) / (sin x))) by A2, FDIFF_8:2, XCMPLX_1:90
.= ((1 / (sin (x + h))) - (sin (x + h))) - ((1 / (sin x)) - (sin x)) by A2, FDIFF_8:2, XCMPLX_1:90
.= (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x) ;
hence (fD f,h) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x) ; :: thesis: verum