A1:
(sqrt (1 / 2)) ^2 = 1 / 2
by SQUARE_1:def 2;
1 =
((sin . (PI / 4)) ^2) + ((sin . (PI / 4)) ^2)
by SIN_COS:28, SIN_COS:73
.=
2 * ((sin . (PI / 4)) ^2)
;
then A2:
( sin . (PI / 4) = sqrt (1 / 2) or sin . (PI / 4) = - (sqrt (1 / 2)) )
by A1, SQUARE_1:40;
PI / 4 < PI / 1
by XREAL_1:76;
then A3:
PI / 4 in ].0,PI.[
;
sqrt (1 / 2) > 0
by SQUARE_1:25;
hence
( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) )
by A2, A3, COMPTRIG:7, SIN_COS:73, SQUARE_1:32; verum