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