theorem :: WALLIS01:33

for n being non zero Nat holds (@ ((@ sin) |^ (n + 1))) `| REAL is_differentiable_on REAL