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:18;
A3: (diff exp_R ,Z) . i is_differentiable_on Z by A2, TAYLOR_1:def 6;
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 8 ;
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:72 ;
hence ((diff (r (#) exp_R ),Z) . n) . x = r * (exp_R . x) ; :: thesis: verum

end;

end;