A1:
(sqrt (1 / 2)) ^2 = 1 / 2
by SQUARE_1:def 4;
1 =
((sin . (PI / 4)) ^2) + ((sin . (PI / 4)) ^2)
by SIN_COS:31, SIN_COS:78
.=
2 * ((sin . (PI / 4)) ^2)
;
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 A3:
PI / 4 in ].0,PI.[
;
sqrt (1 / 2) > 0
by SQUARE_1:93;
hence
( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) )
by A2, A3, COMPTRIG:23, SIN_COS:78, SQUARE_1:101; verum