A1: PI in ].0,4.[ by Def28;
then A2: 0 < PI by XXREAL_1:4;
PI < 4 by A1, XXREAL_1:4;
then PI / 4 < 4 / 4 by XREAL_1:74;
then A3: PI / 4 in ].0,1.[ by A2, XXREAL_1:4;
tan . (PI / 4) = 1 by Def28;
then (sin . (PI / 4)) * ((cos . (PI / 4)) ") = 1 by A3, Th69, RFUNCT_1:def 1;
hence sin . (PI / 4) = cos . (PI / 4) by XCMPLX_1:209; :: thesis: verum