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