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