let Z be open Subset of REAL; ( Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x < 1 ) ) implies ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) )
assume that
A1:
Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos)
and
A2:
for x being Real st x in Z holds
( sin . x > 0 & cos . x < 1 )
; ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) )
Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom cos)
by A1, VALUED_1:12;
then A3:
Z c= dom ((1 / 2) (#) ((#Z 2) * sin))
by XBOOLE_1:18;
then A4:
(1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z
by Th49;
A5:
cos is_differentiable_on Z
by FDIFF_1:26, SIN_COS:67;
now for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x))let x be
Real;
( x in Z implies ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) )assume A6:
x in Z
;
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x))then A7:
1
- (cos . x) > 0
by A2, XREAL_1:50;
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x =
(diff (((1 / 2) (#) ((#Z 2) * sin)),x)) - (diff (cos,x))
by A1, A4, A5, A6, FDIFF_1:19
.=
(diff (((1 / 2) (#) ((#Z 2) * sin)),x)) - (- (sin . x))
by SIN_COS:63
.=
((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) - (- (sin . x))
by A4, A6, FDIFF_1:def 7
.=
((sin . x) * (cos . x)) - (- (sin . x))
by A3, A6, Th49
.=
(((sin . x) * (1 + (cos . x))) * (1 - (cos . x))) / (1 - (cos . x))
by A7, XCMPLX_1:89
.=
((sin . x) * (1 - ((cos . x) ^2))) / (1 - (cos . x))
.=
((sin . x) * (1 - ((cos x) ^2))) / (1 - (cos . x))
by SIN_COS:def 19
.=
((sin . x) * ((sin x) * (sin x))) / (1 - (cos . x))
by SIN_COS4:4
.=
((sin . x) * ((sin x) |^ 2)) / (1 - (cos . x))
by WSIERP_1:1
.=
((sin . x) * ((sin . x) |^ 2)) / (1 - (cos . x))
by SIN_COS:def 17
.=
((sin . x) |^ (2 + 1)) / (1 - (cos . x))
by NEWTON:6
.=
((sin . x) |^ 3) / (1 - (cos . x))
;
hence
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x))
;
verum end;
hence
( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) )
by A1, A4, A5, FDIFF_1:19; verum