let Z be open Subset of REAL; 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; ( 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 )
; ( 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;
( x in Z implies f1 . x = ((- 1) * x) + (- 1) )
assume
x in Z
;
f1 . x = ((- 1) * x) + (- 1)
then f1 . x =
(- x) - 1
by A2
.=
((- 1) * x) + (- 1)
;
hence
f1 . x = ((- 1) * x) + (- 1)
;
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;
( x in Z implies ((f1 (#) (exp_R * f2)) `| Z) . x = x / (exp_R x) )
assume A10:
x in Z
;
((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)
;
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; verum