set h = sec | [.0 ,(PI / 2).[;
A1:
[.0 ,(PI / 4).] c= [.0 ,(PI / 2).[
by Lm5, 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 A1, Th41, RELAT_1:103
;
hence
arcsec1 | [.1,(sqrt 2).] = (sec | [.0 ,(PI / 4).]) "
; verum