theorem :: SINCOS10:54

(sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39;