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

.= Z by Th5 ;

hence (diff (exp_R,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def 6; :: thesis: verum

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

dom ((diff (exp_R,Z)) . i) =
dom (exp_R | Z)
by Th6
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;.= 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

.= Z by Th5 ;

hence (diff (exp_R,Z)) . i is_differentiable_on Z by A1, FDIFF_1:def 6; :: thesis: verum