theorem :: WALLIS01:32

(@ ((@ sin) |^ 1)) `| REAL is_differentiable_on REAL by BINOM:8, INTEGRA8:27, SIN_COS:67;