theorem :: SINCOS10:9

sec | ].0,(PI / 2).[ is continuous by Th5, FDIFF_1:25;