A1: 1 = ((sin . (PI / 4)) ^2 ) + ((sin . (PI / 4)) ^2 ) by SIN_COS:31, SIN_COS:78
.= 2 * ((sin . (PI / 4)) ^2 ) ;
(sqrt (1 / 2)) ^2 = 1 / 2 by SQUARE_1:def 4;
then A2: ( sin . (PI / 4) = sqrt (1 / 2) or sin . (PI / 4) = - (sqrt (1 / 2)) ) by A1, SQUARE_1:109;
PI / 4 < PI / 1 by XREAL_1:78;
then A5: PI / 4 in ].0 ,PI .[ ;
sqrt (1 / 2) > 0 by SQUARE_1:93;
then - (sqrt (1 / 2)) <= - 0 ;
hence ( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) ) by A2, A5, COMPTRIG:23, SIN_COS:78, SQUARE_1:101; :: thesis: verum