set h = sec | [.0 ,(PI / 2).[;
X: [.0 ,(PI / 4).] c= [.0 ,(PI / 2).[ by Lm9, XXREAL_2:def 12;
then (sec | [.0 ,(PI / 4).]) " = ((sec | [.0 ,(PI / 2).[) | [.0 ,(PI / 4).]) " by RELAT_1:103
.= ((sec | [.0 ,(PI / 2).[) " ) | ((sec | [.0 ,(PI / 2).[) .: [.0 ,(PI / 4).]) by RFUNCT_2:40
.= ((sec | [.0 ,(PI / 2).[) " ) | (rng ((sec | [.0 ,(PI / 2).[) | [.0 ,(PI / 4).])) by RELAT_1:148
.= ((sec | [.0 ,(PI / 2).[) " ) | [.1,(sqrt 2).] by Th41, X, RELAT_1:103 ;
hence arcsec1 | [.1,(sqrt 2).] = (sec | [.0 ,(PI / 4).]) " ; :: thesis: verum