let r be Real; :: thesis: for n being Element of NAT holds (#Z n) ^ is_differentiable_on ].0 ,r.[
let n be Element of NAT ; :: thesis: (#Z n) ^ is_differentiable_on ].0 ,r.[
A2: for x0 being Real st x0 in ].0 ,r.[ holds
(#Z n) . x0 <> 0

proof

let x0 be Real; :: thesis: ( x0 in ].0 ,r.[ implies (#Z n) . x0 <> 0 )
assume A3: x0 in ].0 ,r.[ ; :: thesis: (#Z n) . x0 <> 0
A4: x0 <> 0 by A3, XXREAL_1:4;
(#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 ].0 ,r.[ by Th18, FDIFF_1:34;
hence (#Z n) ^ is_differentiable_on ].0 ,r.[ by A2, FDIFF_2:22; :: thesis: verum