theorem Th27: :: WALLIS01:30

for n being non zero Nat holds
( (@ ((@ sin) |^ n)) . 0 = 0 & (@ ((@ sin) |^ n)) . (PI / 2) = 1 )