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:74
.=
((sec | [.0,(PI / 2).[) ") | ((sec | [.0,(PI / 2).[) .: [.0,(PI / 4).])
by RFUNCT_2:17
.=
((sec | [.0,(PI / 2).[) ") | (rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 4).]))
by RELAT_1:115
.=
((sec | [.0,(PI / 2).[) ") | [.1,(sqrt 2).]
by A1, Th41, RELAT_1:74
;
hence
arcsec1 | [.1,(sqrt 2).] = (sec | [.0,(PI / 4).]) "
; verum