theorem :: SIN_COS9:9

tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:8;