theorem Th65: :: SINCOS10:65

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