theorem :: SINCOS10:57

(sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39;