theorem :: SIN_COS9:27

(tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by Th21, Th25, FUNCT_1:39;