let x, r be Real; :: thesis: for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)
let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st x in Z holds
((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)
let Z be open Subset of REAL; :: thesis: ( x in Z implies ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) )
assume A1: x in Z ; :: thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)
A2: exp_R is_differentiable_on n,Z by TAYLOR_2:10;

per cases ( n > 0 or n = 0 ) ;

suppose n > 0 ; :: thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)

then 0 < 0 + n ;
then 1 <= n by NAT_1:19;
then reconsider i = n - 1 as Element of NAT by INT_1:5;
A3: (diff (exp_R,Z)) . i is_differentiable_on Z by A2;
dom ((diff (exp_R,Z)) . n) = dom ((diff (exp_R,Z)) . (i + 1))
.= dom (((diff (exp_R,Z)) . i) `| Z) by TAYLOR_1:def 5
.= Z by A3, FDIFF_1:def 7 ;
then A4: x in dom (r (#) ((diff (exp_R,Z)) . n)) by A1, VALUED_1:def 5;
((diff ((r (#) exp_R),Z)) . n) . x = (r (#) ((diff (exp_R,Z)) . n)) . x by Th21, TAYLOR_2:10
.= r * (((diff (exp_R,Z)) . n) . x) by A4, VALUED_1:def 5
.= r * (exp_R . x) by A1, TAYLOR_2:7 ;
hence ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) ; :: thesis: verum

end;

suppose A5: n = 0 ; :: thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)

A6: dom (r (#) (exp_R | Z)) = dom (exp_R | Z) by VALUED_1:def 5
.= Z by Th1 ;
((diff ((r (#) exp_R),Z)) . n) . x = (r (#) ((diff (exp_R,Z)) . 0)) . x by A5, Th21, TAYLOR_2:10
.= (r (#) (exp_R | Z)) . x by TAYLOR_1:def 5
.= r * ((exp_R | Z) . x) by A1, A6, VALUED_1:def 5
.= r * (exp_R . x) by A1, FUNCT_1:49 ;
hence ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) ; :: thesis: verum

end;

end;