defpred S1[ set , set ] means for p being Point of (TOP-REAL 2) st p = $1 holds
( ( p = 0. (TOP-REAL 2) implies $2 = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies $2 = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or $2 = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) );
set BP = the carrier of (TOP-REAL 2);
A1:
for x being Element of the carrier of (TOP-REAL 2) ex y being Element of the carrier of (TOP-REAL 2) st S1[x,y]
ex h being Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) st
for x being Element of the carrier of (TOP-REAL 2) holds S1[x,h . x]
from FUNCT_2:sch 3(A1);
then consider h being Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) such that
A4:
for x being Element of the carrier of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p = x holds
( ( p = 0. (TOP-REAL 2) implies h . x = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h . x = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h . x = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )
;
for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies h . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )
by A4;
hence
ex b1 being Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2) st
for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies b1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies b1 . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or b1 . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) )
; verum