theorem :: SINCOS10:21

sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8;