theorem Th24: :: WALLIS01:27

for Z being open Subset of REAL
for n being non zero Nat
for x being Function of REAL,REAL st x is_differentiable_on Z holds
@ ((@ x) |^ n) is_differentiable_on Z