let n be non zero Nat; :: thesis: ( (@ ((@ sin) |^ n)) . 0 = 0 & (@ ((@ sin) |^ n)) . (PI / 2) = 1 )
A1: (@ (@ sin)) . 0 = 0 by SIN_COS:30;
(@ (@ sin)) . (PI / 2) = 1 by SIN_COS:76;
then (@ ((@ sin) |^ n)) . (PI / 2) = 1 |^ n by Th22
.= 1 ;
hence ( (@ ((@ sin) |^ n)) . 0 = 0 & (@ ((@ sin) |^ n)) . (PI / 2) = 1 ) by A1, Th23; :: thesis: verum