set h = sec | ].(PI / 2),PI.];
A1: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def 12;
then (sec | [.((3 / 4) * PI),PI.]) " = ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.]) " by RELAT_1:74
.= ((sec | ].(PI / 2),PI.]) ") | ((sec | ].(PI / 2),PI.]) .: [.((3 / 4) * PI),PI.]) by RFUNCT_2:17
.= ((sec | ].(PI / 2),PI.]) ") | (rng ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.])) by RELAT_1:115
.= ((sec | ].(PI / 2),PI.]) ") | [.(- (sqrt 2)),(- 1).] by A1, Th42, RELAT_1:74 ;
hence arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI),PI.]) " ; :: thesis: verum