PI in ].0 ,4.[ by Def32;
then ( 0 < PI & PI < 4 ) by XXREAL_1:4;
then ( 0 / 4 < PI / 4 & PI / 4 < 4 / 4 ) by XREAL_1:76;
then A1: PI / 4 in ].0 ,1.[ by XXREAL_1:4;
tan . (PI / 4) = 1 by Def32;
then (sin . (PI / 4)) * ((cos . (PI / 4)) " ) = 1 by A1, Th75, RFUNCT_1:def 4;
hence sin . (PI / 4) = cos . (PI / 4) by XCMPLX_1:210; :: thesis: verum