theorem Th31: :: SIN_COS9:31

arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by Lm5, Th11, FUNCT_1:39;