reconsider BP = the carrier of (TOP-REAL 2) \ {(0.REAL 2)} as non empty set by Th19;
defpred S₁[ set , set ] means for p being Point of (TOP-REAL 2) st p = $1 holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies $2 = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or $2 = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) );
A1: for x being Element of BP ex y being Element of BP st S₁[x,y]

proof

let x be Element of BP; :: thesis: ex y being Element of BP st S₁[x,y]
reconsider q = x as Point of (TOP-REAL 2) by TARSKI:def 3;

now

per cases ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) or ( not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ) ;

case A2: ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: ex y being Element of BP st
for p being Point of (TOP-REAL 2) st p = x holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies y = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or y = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) )

now

assume |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| in {(0.REAL 2)} ; :: thesis: contradiction
then 0.REAL 2 = |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| by TARSKI:def 1;
then ( 0 = 1 / (q `1 ) & 0 = ((q `2 ) / (q `1 )) / (q `1 ) ) by Th11, EUCLID:56;
then A3: 0 = (1 / (q `1 )) * (q `1 ) ;

now

per cases ( q `1 = 0 or q `1 <> 0 ) ;

case A4: q `1 = 0 ; :: thesis: contradiction

then q `2 = 0 by A2;
then q = 0.REAL 2 by A4, EUCLID:57, EUCLID:58;
then q in {(0.REAL 2)} by TARSKI:def 1;
hence contradiction by XBOOLE_0:def 5; :: thesis: verum

end;

case q `1 <> 0 ; :: thesis: contradiction

hence contradiction by A3, XCMPLX_1:88; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

then reconsider r = |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| as Element of BP by XBOOLE_0:def 5;
for p being Point of (TOP-REAL 2) st p = x holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies r = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or r = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) by A2;
hence ex y being Element of BP st
for p being Point of (TOP-REAL 2) st p = x holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies y = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or y = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ; :: thesis: verum

end;

case A5: ( not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: ex y being Element of BP st S₁[x,y]

now

assume |[(((q `1 ) / (q `2 )) / (q `2 )),(1 / (q `2 ))]| in {(0.REAL 2)} ; :: thesis: contradiction
then 0.REAL 2 = |[(((q `1 ) / (q `2 )) / (q `2 )),(1 / (q `2 ))]| by TARSKI:def 1;
then ( (0.REAL 2) `2 = 1 / (q `2 ) & (0.REAL 2) `1 = ((q `1 ) / (q `2 )) / (q `2 ) ) by EUCLID:56;
then A6: 0 = (1 / (q `2 )) * (q `2 ) by Th11;
q `2 <> 0 by A5;
hence contradiction by A6, XCMPLX_1:88; :: thesis: verum

end;

then reconsider r = |[(((q `1 ) / (q `2 )) / (q `2 )),(1 / (q `2 ))]| as Element of BP by XBOOLE_0:def 5;
for p being Point of (TOP-REAL 2) st p = x holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies r = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or r = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) by A5;
hence ex y being Element of BP st S₁[x,y] ; :: thesis: verum

end;

end;

end;

hence ex y being Element of BP st S₁[x,y] ; :: thesis: verum

end;

ex h being Function of BP,BP st
for x being Element of BP holds S₁[x,h . x] from FUNCT_2:sch 3(A1);
then consider h being Function of BP,BP such that
A7: for x being Element of BP
for p being Point of (TOP-REAL 2) st p = x holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies h . x = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or h . x = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ;
for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies h . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or h . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) )

proof

let p be Point of (TOP-REAL 2); :: thesis: ( p <> 0.REAL 2 implies ( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies h . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or h . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) )
assume p <> 0.REAL 2 ; :: thesis: ( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies h . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or h . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) )
then not p in {(0.REAL 2)} by TARSKI:def 1;
then p in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} by XBOOLE_0:def 5;
hence ( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies h . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or h . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) by A7; :: thesis: verum

end;

hence ex b₁ being Function of the carrier of (TOP-REAL 2) \ {(0.REAL 2)},the carrier of (TOP-REAL 2) \ {(0.REAL 2)} st
for p being Point of (TOP-REAL 2) st p <> 0.REAL 2 holds
( ( ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) ) implies b₁ . p = |[(1 / (p `1 )),(((p `2 ) / (p `1 )) / (p `1 ))]| ) & ( ( p `2 <= p `1 & - (p `1 ) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1 ) ) or b₁ . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ; :: thesis: verum