let Z be open Subset of REAL; :: thesis: for n being Element of NAT holds exp_R is_differentiable_on n,Z
let n be Element of NAT ; :: thesis: exp_R is_differentiable_on n,Z
let i be Nat; :: according to TAYLOR_1:def 6 :: thesis: ( not i <= n - 1 or (diff (exp_R,Z)) . i is_differentiable_on Z )
assume i <= n - 1 ; :: thesis: (diff (exp_R,Z)) . i is_differentiable_on Z
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A1: for x being Real st x in Z holds
((diff (exp_R,Z)) . i) | Z is_differentiable_in x

proof

A2: ((diff (exp_R,Z)) . i) | Z = (exp_R | Z) | Z by Th6
.= exp_R | Z by FUNCT_1:51 ;
A3: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16;
let x be Real; :: thesis: ( x in Z implies ((diff (exp_R,Z)) . i) | Z is_differentiable_in x )
assume x in Z ; :: thesis: ((diff (exp_R,Z)) . i) | Z is_differentiable_in x
hence ((diff (exp_R,Z)) . i) | Z is_differentiable_in x by A2, A3, FDIFF_1:def 6; :: thesis: verum

end;

dom ((diff (exp_R,Z)) . i) = dom (exp_R | Z) by Th6
.= Z by Th5 ;
hence (diff (exp_R,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def 6; :: thesis: verum