let Z be open Subset of REAL; :: thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 (#) (exp_R * f2)) & ( for x being Real st x in Z holds
( f1 . x = (- x) - 1 & f2 . x = - x ) ) holds
( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( Z c= dom (f1 (#) (exp_R * f2)) & ( for x being Real st x in Z holds
( f1 . x = (- x) - 1 & f2 . x = - x ) ) implies ( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) ) )
assume that
A1: Z c= dom (f1 (#) (exp_R * f2)) and
A2: for x being Real st x in Z holds
( f1 . x = (- x) - 1 & f2 . x = - x ) ; :: thesis: ( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) )
A3: Z c= (dom f1) /\ (dom (exp_R * f2)) by A1, VALUED_1:def 4;
then A4: Z c= dom f1 by XBOOLE_1:18;
A5: Z c= dom (exp_R * f2) by A3, XBOOLE_1:18;
A6: for x being Real st x in Z holds
f1 . x = ((- 1) * x) + (- 1)

proof

let x be Real; :: thesis: ( x in Z implies f1 . x = ((- 1) * x) + (- 1) )
assume x in Z ; :: thesis: f1 . x = ((- 1) * x) + (- 1)
then f1 . x = (- x) - 1 by A2
.= ((- 1) * x) + (- 1) ;
hence f1 . x = ((- 1) * x) + (- 1) ; :: thesis: verum

end;

then A7: f1 is_differentiable_on Z by A4, FDIFF_1:23;
A8: for x being Real st x in Z holds
f2 . x = - x by A2;
then A9: exp_R * f2 is_differentiable_on Z by A5, Th14;
for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x)

proof

let x be Real; :: thesis: ( x in Z implies ((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) )
assume A10: x in Z ; :: thesis: ((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x)
then A11: (exp_R * f2) . x = exp_R . (f2 . x) by A5, FUNCT_1:12
.= exp_R . (- x) by A2, A10
.= exp_R (- x) by SIN_COS:def 23 ;
((f1 (#) (exp_R * f2)) `| Z) . x = (((exp_R * f2) . x) * (diff (f1,x))) + ((f1 . x) * (diff ((exp_R * f2),x))) by A1, A7, A9, A10, FDIFF_1:21
.= ((exp_R (- x)) * (diff (f1,x))) + (((- x) - 1) * (diff ((exp_R * f2),x))) by A2, A10, A11
.= ((exp_R (- x)) * ((f1 `| Z) . x)) + (((- x) - 1) * (diff ((exp_R * f2),x))) by A7, A10, FDIFF_1:def 7
.= ((exp_R (- x)) * ((f1 `| Z) . x)) + (((- x) - 1) * (((exp_R * f2) `| Z) . x)) by A9, A10, FDIFF_1:def 7
.= ((exp_R (- x)) * (- 1)) + (((- x) - 1) * (((exp_R * f2) `| Z) . x)) by A4, A6, A10, FDIFF_1:23
.= ((exp_R (- x)) * (- 1)) + (((- x) - 1) * (- (exp_R (- x)))) by A8, A5, A10, Th14
.= x * (exp_R (- x))
.= x * (1 / (exp_R x)) by TAYLOR_1:4
.= x / (exp_R x) by XCMPLX_1:99 ;
hence ((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ; :: thesis: verum

end;

hence ( f1 (#) (exp_R * f2) is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) ) ) by A1, A7, A9, FDIFF_1:21; :: thesis: verum