let Z be open Subset of REAL ; ( Z c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos ) implies ( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) ) )
assume A1:
Z c= dom (((1 / 3) (#) ((#Z 3) * cos )) - cos )
; ( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) )
then
Z c= (dom ((1 / 3) (#) ((#Z 3) * cos ))) /\ (dom cos )
by VALUED_1:12;
then A2:
Z c= dom ((1 / 3) (#) ((#Z 3) * cos ))
by XBOOLE_1:18;
then A3:
(1 / 3) (#) ((#Z 3) * cos ) is_differentiable_on Z
by Th46;
A4:
cos is_differentiable_on Z
by FDIFF_1:34, SIN_COS:72;
now let x be
Real;
( x in Z implies ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 )assume A5:
x in Z
;
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3then ((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x =
(diff ((1 / 3) (#) ((#Z 3) * cos )),x) - (diff cos ,x)
by A1, A3, A4, FDIFF_1:27
.=
(diff ((1 / 3) (#) ((#Z 3) * cos )),x) - (- (sin . x))
by SIN_COS:68
.=
((((1 / 3) (#) ((#Z 3) * cos )) `| Z) . x) - (- (sin . x))
by A3, A5, FDIFF_1:def 8
.=
(- (((cos . x) #Z (3 - 1)) * (sin . x))) - (- (sin . x))
by A2, A5, Th46
.=
(sin . x) * (1 - ((cos . x) #Z 2))
.=
(sin . x) * (1 - ((cos . x) |^ (abs 2)))
by PREPOWER:def 4
.=
(sin . x) * (1 - ((cos . x) |^ 2))
by ABSVALUE:def 1
.=
(sin . x) * (1 - ((cos . x) * (cos . x)))
by WSIERP_1:2
.=
(sin . x) * ((((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) - ((cos . x) * (cos . x)))
by SIN_COS:31
.=
(sin . x) * ((sin . x) |^ 2)
by WSIERP_1:2
.=
(sin . x) |^ (2 + 1)
by NEWTON:11
.=
(sin . x) |^ 3
;
hence
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3
;
verum end;
hence
( ((1 / 3) (#) ((#Z 3) * cos )) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 3) (#) ((#Z 3) * cos )) - cos ) `| Z) . x = (sin . x) |^ 3 ) )
by A1, A3, A4, FDIFF_1:27; verum