defpred S₁[ 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 S₁[x,y]

proof

let x be Element of the carrier of (TOP-REAL 2); :: thesis: ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y]
set q = x;

per cases ( x = 0. (TOP-REAL 2) or ( ( ( x `2 <= x `1 & - (x `1 ) <= x `2 ) or ( x `2 >= x `1 & x `2 <= - (x `1 ) ) ) & x <> 0. (TOP-REAL 2) ) or ( not ( x `2 <= x `1 & - (x `1 ) <= x `2 ) & not ( x `2 >= x `1 & x `2 <= - (x `1 ) ) & x <> 0. (TOP-REAL 2) ) ) ;

suppose x = 0. (TOP-REAL 2) ; :: thesis: ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y]

then for p being Point of (TOP-REAL 2) st p = x holds
( ( p = 0. (TOP-REAL 2) implies 0. (TOP-REAL 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 0. (TOP-REAL 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 0. (TOP-REAL 2) = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ;
hence ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y] ; :: thesis: verum

end;

suppose A2: ( ( ( x `2 <= x `1 & - (x `1 ) <= x `2 ) or ( x `2 >= x `1 & x `2 <= - (x `1 ) ) ) & x <> 0. (TOP-REAL 2) ) ; :: thesis: ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y]

set r = |[((x `1 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 ))))]|;
for p being Point of (TOP-REAL 2) st p = x holds
( ( p = 0. (TOP-REAL 2) implies |[((x `1 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^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 |[((x `1 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^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 |[((x `1 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `2 ) / (x `1 )) ^2 ))))]| = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) by A2;
hence ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y] ; :: thesis: verum

end;

suppose A3: ( not ( x `2 <= x `1 & - (x `1 ) <= x `2 ) & not ( x `2 >= x `1 & x `2 <= - (x `1 ) ) & x <> 0. (TOP-REAL 2) ) ; :: thesis: ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y]

set r = |[((x `1 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 ))))]|;
for p being Point of (TOP-REAL 2) st p = x holds
( ( p = 0. (TOP-REAL 2) implies |[((x `1 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^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 |[((x `1 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^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 |[((x `1 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 )))),((x `2 ) / (sqrt (1 + (((x `1 ) / (x `2 )) ^2 ))))]| = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) by A3;
hence ex y being Element of the carrier of (TOP-REAL 2) st S₁[x,y] ; :: thesis: verum

end;

end;

end;

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 S₁[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 b₁ 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 b₁ . 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 b₁ . 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 b₁ . p = |[((p `1 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 )))),((p `2 ) / (sqrt (1 + (((p `1 ) / (p `2 )) ^2 ))))]| ) ) ; :: thesis: verum