let Z be open Subset of REAL; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( ((#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;

A5: now :: thesis: for x being Real st x in Z holds
(#Z 2) * exp_R is_differentiable_in x

let x be Real; :: thesis: ( x in Z implies (#Z 2) * exp_R is_differentiable_in x )
assume x in Z ; :: thesis: (#Z 2) * exp_R is_differentiable_in x
exp_R is_differentiable_in x by SIN_COS:65;
hence (#Z 2) * exp_R is_differentiable_in x by TAYLOR_1:3; :: thesis: verum

end;

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; :: thesis: ( 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 ; :: thesis: ((((#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)) ; :: thesis: 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; :: thesis: verum