A1: arctan 1 = arctan (tan . (PI / 4)) by SIN_COS:def 32;
( - (PI / 2) < PI / 4 & PI / 4 < PI / 2 ) by Lm8, XXREAL_1:4;
hence ( arctan 1 = PI / 4 & arctan . 1 = PI / 4 ) by A1, Th33; :: thesis: verum