reconsider BP = NonZero (TOP-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 S₁[x,y]

now

assume |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| in {(0. (TOP-REAL 2))} ; :: thesis: contradiction
then 0. (TOP-REAL 2) = |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| by TARSKI:def 1;
then 0 = 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. (TOP-REAL 2) by A4, EUCLID:57, EUCLID:58;
then q in {(0. (TOP-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 S₁[x,y] ; :: 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. (TOP-REAL 2))} ; :: thesis: contradiction
then 0. (TOP-REAL 2) = |[(((q `1 ) / (q `2 )) / (q `2 )),(1 / (q `2 ))]| by TARSKI:def 1;
then (0. (TOP-REAL 2)) `2 = 1 / (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. (TOP-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. (TOP-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. (TOP-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. (TOP-REAL 2))} by TARSKI:def 1;
then p in NonZero (TOP-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 (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)) st
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-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