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