@ ((@ sin) |^ 1) = sin by BINOM:8;
then integral ((@ ((@ sin) |^ 1)),0,(PI / 2)) = 1 - 0 by SIN_COS:76, SIN_COS:30, INTEGRA7:26;
hence integral ((@ ((@ sin) |^ 1)),0,(PI / 2)) = 1 ; :: thesis: verum