theorem Th31: :: WALLIS01:34

for n being Nat st n >= 2 holds
@ ((@ sin) |^ (n -' 1)) is_integral_of ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)), REAL