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)) ) )
Z c= (dom ((#Z 2) * exp_R )) /\ (dom f) by A1, VALUED_1:def 1;
then A3: ( Z c= dom ((#Z 2) * exp_R ) & Z c= dom f ) by XBOOLE_1:18;
A4: for x being Real st x in Z holds
f . x = (0 * x) + 1 by A2;
then A5: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = 0 ) ) by A3, FDIFF_1:31;

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;

then A6: (#Z 2) * exp_R is_differentiable_on Z by A3, 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)) )
assume A7: x in Z ; :: thesis: ((((#Z 2) * exp_R ) + f) `| Z) . x = 2 * (exp_R (2 * x))
A8: exp_R is_differentiable_in x by SIN_COS:70;
((((#Z 2) * exp_R ) + f) `| Z) . x = (diff ((#Z 2) * exp_R ),x) + (diff f,x) by A1, A5, A6, A7, FDIFF_1:26
.= ((2 * ((exp_R . x) #Z (2 - 1))) * (diff exp_R ,x)) + (diff f,x) by A8, 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 A5, A7, FDIFF_1:def 8
.= (2 * (exp_R (2 * x))) + 0 by A3, A4, A7, 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, A5, A6, FDIFF_1:26; :: thesis: verum