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