let Z be open Subset of REAL; for f being PartFunc of REAL,REAL st Z c= dom (((#Z 2) * exp_R) + f) & ( for x being Real st x in Z holds
f . x = 1 ) holds
( ((#Z 2) * exp_R) + f is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) ) )
let f be PartFunc of REAL,REAL; ( Z c= dom (((#Z 2) * exp_R) + f) & ( for x being Real st x in Z holds
f . x = 1 ) implies ( ((#Z 2) * exp_R) + f is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) ) ) )
assume that
A1:
Z c= dom (((#Z 2) * exp_R) + f)
and
A2:
for x being Real st x in Z holds
f . x = 1
; ( ((#Z 2) * exp_R) + f is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) ) )
A3:
Z c= (dom ((#Z 2) * exp_R)) /\ (dom f)
by A1, VALUED_1:def 1;
then A4:
Z c= dom f
by XBOOLE_1:18;
A6:
for x being Real st x in Z holds
f . x = (0 * x) + 1
by A2;
then A7:
f is_differentiable_on Z
by A4, FDIFF_1:23;
Z c= dom ((#Z 2) * exp_R)
by A3, XBOOLE_1:18;
then A8:
(#Z 2) * exp_R is_differentiable_on Z
by A5, FDIFF_1:9;
for x being Real st x in Z holds
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x))
proof
let x be
Real;
( x in Z implies ((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) )
A9:
exp_R is_differentiable_in x
by SIN_COS:65;
assume A10:
x in Z
;
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x))
then ((((#Z 2) * exp_R) + f) `| Z) . x =
(diff (((#Z 2) * exp_R),x)) + (diff (f,x))
by A1, A7, A8, FDIFF_1:18
.=
((2 * ((exp_R . x) #Z (2 - 1))) * (diff (exp_R,x))) + (diff (f,x))
by A9, TAYLOR_1:3
.=
((2 * ((exp_R . x) #Z (2 - 1))) * (exp_R . x)) + (diff (f,x))
by SIN_COS:65
.=
((2 * (exp_R . x)) * (exp_R . x)) + (diff (f,x))
by PREPOWER:35
.=
(2 * ((exp_R . x) * (exp_R . x))) + (diff (f,x))
.=
(2 * ((exp_R x) * (exp_R . x))) + (diff (f,x))
by SIN_COS:def 23
.=
(2 * ((exp_R x) * (exp_R x))) + (diff (f,x))
by SIN_COS:def 23
.=
(2 * (exp_R (x + x))) + (diff (f,x))
by SIN_COS:50
.=
(2 * (exp_R (2 * x))) + ((f `| Z) . x)
by A7, A10, FDIFF_1:def 7
.=
(2 * (exp_R (2 * x))) + 0
by A4, A6, A10, FDIFF_1:23
.=
2
* (exp_R (2 * x))
;
hence
((((#Z 2) * exp_R) + f) `| Z) . x = 2
* (exp_R (2 * x))
;
verum
end;
hence
( ((#Z 2) * exp_R) + f is_differentiable_on Z & ( for x being Real st x in Z holds
((((#Z 2) * exp_R) + f) `| Z) . x = 2 * (exp_R (2 * x)) ) )
by A1, A7, A8, FDIFF_1:18; verum