tan .: ].(- (PI / 2)),(PI / 2).[ = rng (tan | ].(- (PI / 2)),(PI / 2).[) by RELAT_1:115
.= dom arctan by Th1, FUNCT_2:def 1 ;
hence arctan is differentiable by FDIFF_1:def 8, SIN_COS9:71; :: thesis: verum