set h = cosec | ].0,(PI / 2).];
A1: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def 12;
then (cosec | [.(PI / 4),(PI / 2).]) " = ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).]) " by RELAT_1:74
.= ((cosec | ].0,(PI / 2).]) ") | ((cosec | ].0,(PI / 2).]) .: [.(PI / 4),(PI / 2).]) by RFUNCT_2:17
.= ((cosec | ].0,(PI / 2).]) ") | (rng ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).])) by RELAT_1:115
.= ((cosec | ].0,(PI / 2).]) ") | [.1,(sqrt 2).] by A1, Th44, RELAT_1:74 ;
hence arccosec2 | [.1,(sqrt 2).] = (cosec | [.(PI / 4),(PI / 2).]) " ; :: thesis: verum