theorem Th28: :: WALLIS01:31

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