let Z be open Subset of REAL ; :: thesis: ( Z c= dom ((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) & ( for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ) implies ( (- cos ) - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) )
assume that
A1: Z c= dom ((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) and
A2: for x being Real st x in Z holds
( sin . x > 0 & cos . x > - 1 ) ; :: thesis: ( (- cos ) - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| 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 )) & Z c= dom (- cos ) ) by XBOOLE_1:18;
then A4: ( (1 / 2) (#) ((#Z 2) * sin ) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) ((#Z 2) * sin )) `| Z) . x = (sin . x) * (cos . x) ) ) by Th49;
A5: (- 1) (#) cos = - cos ;
A6: cos is_differentiable_on Z by FDIFF_1:34, SIN_COS:72;
then A7: ( - cos is_differentiable_on Z & ( for x being Real st x in Z holds
((- cos ) `| Z) . x = (- 1) * (diff cos ,x) ) ) by A3, A5, FDIFF_1:28;

now

let x be Real; :: thesis: ( x in Z implies (((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) )
assume A8: x in Z ; :: thesis: (((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x))
then cos . x > - 1 by A2;
then A9: (cos . x) - (- 1) > 0 by XREAL_1:52;
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = (diff (- cos ),x) - (diff ((1 / 2) (#) ((#Z 2) * sin )),x) by A1, A4, A7, A8, FDIFF_1:27
.= (((- cos ) `| Z) . x) - (diff ((1 / 2) (#) ((#Z 2) * sin )),x) by A7, A8, FDIFF_1:def 8
.= ((- 1) * (diff cos ,x)) - (diff ((1 / 2) (#) ((#Z 2) * sin )),x) by A3, A6, A8, FDIFF_1:28
.= ((- 1) * (- (sin . x))) - (diff ((1 / 2) (#) ((#Z 2) * sin )),x) by SIN_COS:68
.= (sin . x) - ((((1 / 2) (#) ((#Z 2) * sin )) `| Z) . x) by A4, A8, FDIFF_1:def 8
.= (sin . x) - ((sin . x) * (cos . x)) by A3, A8, Th49
.= (((sin . x) * (1 - (cos . x))) * (1 + (cos . x))) / (1 + (cos . x)) by A9, XCMPLX_1:90
.= ((sin . x) * (1 - ((cos . x) ^2 ))) / (1 + (cos . x))
.= ((sin . x) * (1 - ((cos x) ^2 ))) / (1 + (cos . x)) by SIN_COS:def 23
.= ((sin . x) * ((sin x) * (sin x))) / (1 + (cos . x)) by SIN_COS4:6
.= ((sin . x) * ((sin x) |^ 2)) / (1 + (cos . x)) by WSIERP_1:2
.= ((sin . x) * ((sin . x) |^ 2)) / (1 + (cos . x)) by SIN_COS:def 21
.= ((sin . x) |^ (2 + 1)) / (1 + (cos . x)) by NEWTON:11
.= ((sin . x) |^ 3) / (1 + (cos . x)) ;
hence (((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ; :: thesis: verum

end;

hence ( (- cos ) - ((1 / 2) (#) ((#Z 2) * sin )) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cos ) - ((1 / 2) (#) ((#Z 2) * sin ))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) by A1, A4, A7, FDIFF_1:27; :: thesis: verum