let Z be open Subset of REAL; :: thesis: ( Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) implies ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) ) )
assume A1: Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) ; :: thesis: ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) )
then A2: Z c= dom ((sin + cos) / exp_R) by VALUED_1:def 5;
then Z c= (dom (sin + cos)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def 1;
then A3: Z c= dom (sin + cos) by XBOOLE_1:18;
then A4: ( sin + cos is_differentiable_on Z & ( for x being Real st x in Z holds
((sin + cos) `| Z) . x = (cos . x) - (sin . x) ) ) by FDIFF_7:38;
A5: (sin + cos) / exp_R is_differentiable_on Z by A2, FDIFF_7:42;
then A6: (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z by FDIFF_2:19;
for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x)

proof

let x be Real; :: thesis: ( x in Z implies (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) )
A7: x in REAL by XREAL_0:def 1;
assume A8: x in Z ; :: thesis: (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x)
A9: exp_R is_differentiable_in x by SIN_COS:65;
A10: sin + cos is_differentiable_in x by A4, A8, FDIFF_1:9;
A11: (sin + cos) . x = (sin . x) + (cos . x) by VALUED_1:1, A7;
A12: exp_R . x <> 0 by SIN_COS:54;
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (- (1 / 2)) * (diff (((sin + cos) / exp_R),x)) by A1, A5, A8, FDIFF_1:20
.= (- (1 / 2)) * ((((diff ((sin + cos),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A9, A10, A12, FDIFF_2:14
.= (- (1 / 2)) * ((((((sin + cos) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A4, A8, FDIFF_1:def 7
.= (- (1 / 2)) * (((((cos . x) - (sin . x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((sin + cos) . x))) / ((exp_R . x) ^2)) by A3, A8, FDIFF_7:38
.= (- (1 / 2)) * (((((cos . x) - (sin . x)) * (exp_R . x)) - ((exp_R . x) * ((sin . x) + (cos . x)))) / ((exp_R . x) ^2)) by A11, SIN_COS:65
.= (- (1 / 2)) * ((- (2 * (sin . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))))
.= (- (1 / 2)) * ((- (2 * (sin . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x))) by XCMPLX_1:78
.= (- (1 / 2)) * ((- (2 * (sin . x))) * (1 / (exp_R . x))) by A12, XCMPLX_1:60
.= (sin . x) / (exp_R . x) ;
hence (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ; :: thesis: verum

end;

hence ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) ) by A6; :: thesis: verum