theorem :: SIN_COS9:77

arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is continuous by Th71, FDIFF_1:25;