theorem :: SINCOS10:61

arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39;