let Z be open Subset of REAL; :: thesis: ( Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds
( sin . x > 0 & sin . x < 1 ) ) implies ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) )
assume that
A1: Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) and
A2: for x being Real st x in Z holds
( sin . x > 0 & sin . x < 1 ) ; :: thesis: ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) )
Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom sin) by A1, VALUED_1:def 1;
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: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68;

now :: thesis: for x being Real st x in Z holds
((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x))

let x be Real; :: thesis: ( x in Z implies ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) )
assume A6: x in Z ; :: thesis: ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x))
then sin . x < 1 by A2;
then A7: 1 - (sin . x) > 0 by XREAL_1:50;
((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = (diff (sin,x)) + (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A1, A4, A5, A6, FDIFF_1:18
.= (cos . x) + (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by SIN_COS:64
.= (cos . x) + ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) by A4, A6, FDIFF_1:def 7
.= (cos . x) + ((sin . x) * (cos . x)) by A3, A6, Th49
.= (((cos . x) * (1 + (sin . x))) * (1 - (sin . x))) / (1 - (sin . x)) by A7, XCMPLX_1:89
.= ((cos . x) * (1 - ((sin . x) ^2))) / (1 - (sin . x))
.= ((cos . x) * (1 - ((sin x) ^2))) / (1 - (sin . x)) by SIN_COS:def 17
.= ((cos . x) * ((cos x) * (cos x))) / (1 - (sin . x)) by SIN_COS4:5
.= ((cos . x) * ((cos x) |^ 2)) / (1 - (sin . x)) by WSIERP_1:1
.= ((cos . x) * ((cos . x) |^ 2)) / (1 - (sin . x)) by SIN_COS:def 19
.= ((cos . x) |^ (2 + 1)) / (1 - (sin . x)) by NEWTON:6
.= ((cos . x) |^ 3) / (1 - (sin . x)) ;
hence ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ; :: thesis: verum

end;

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