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 )
A3: (#Z n) . x0 = x0 #Z n by TAYLOR_1:def 1;
assume x0 in Z ; :: thesis: (#Z n) . x0 <> 0
hence (#Z n) . x0 <> 0 by A1, A3, PREPOWER:38; :: thesis: verum
end;
#Z n is_differentiable_on Z by Th8, FDIFF_1:26;
hence (#Z n) ^ is_differentiable_on Z by A2, FDIFF_2:22; :: thesis: verum