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