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

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:70;
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:31;
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:16;
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:70;
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:26
.= ((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:70
.= ((2 * (exp_R . x)) * (exp_R . x)) + (diff f,x) by PREPOWER:45
.= (2 * ((exp_R . x) * (exp_R . x))) + (diff f,x)
.= (2 * ((exp_R x) * (exp_R . x))) + (diff f,x) by SIN_COS:def 27
.= (2 * ((exp_R x) * (exp_R x))) + (diff f,x) by SIN_COS:def 27
.= (2 * (exp_R (x + x))) + (diff f,x) by SIN_COS:55
.= (2 * (exp_R (2 * x))) + ((f `| Z) . x) by A7, A10, FDIFF_1:def 8
.= (2 * (exp_R (2 * x))) + 0 by A4, A6, A10, FDIFF_1:31
.= 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:26; :: thesis: verum