let n be Element of NAT ; :: thesis: for Z being open Subset of REAL st not 0 in Z holds
(#Z n) ^ is_differentiable_on Z
let Z be open Subset of REAL ; :: thesis: ( not 0 in Z implies (#Z n) ^ is_differentiable_on Z )
assume A1: not 0 in Z ; :: thesis: (#Z n) ^ is_differentiable_on Z
A2: for x0 being Real st x0 in Z holds
(#Z n) . x0 <> 0

proof

let x0 be Real; :: thesis: ( x0 in Z implies (#Z n) . x0 <> 0 )
assume x0 in Z ; :: thesis: (#Z n) . x0 <> 0
then A4: x0 <> 0 by A1;
(#Z n) . x0 = x0 #Z n by TAYLOR_1:def 1;
hence (#Z n) . x0 <> 0 by A4, PREPOWER:48; :: thesis: verum

end;

#Z n is_differentiable_on Z by Th18, FDIFF_1:34;
hence (#Z n) ^ is_differentiable_on Z by A2, FDIFF_2:22; :: thesis: verum