theorem Th35: :: WALLIS01:38

( ((@ sin) |^ 2) + ((@ cos) |^ 2) = 1. (RAlgebra REAL) & (@ sin) |^ 2 = sin (#) sin & (@ cos) |^ 2 = cos (#) cos & (@ sin) |^ 2 = (@ sin) * (@ sin) & (@ cos) |^ 2 = (@ cos) * (@ cos) )