theorem :: SINCOS10:62

arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39;