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