reconsider BP = NonZero (TOP-REAL 2) as non empty set by Th9;
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 :: thesis: ( ( ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) & ex y being Element of BP st S₁[x,y] ) or ( not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) & ex y being Element of BP st S₁[x,y] ) )

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 :: thesis: not |[(1 / (q `1)),(((q `2) / (q `1)) / (q `1))]| in {(0. (TOP-REAL 2))}

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 Th3, EUCLID:52;
then A3: 0 = (1 / (q `1)) * (q `1) ;

now :: thesis: ( ( q `1 = 0 & contradiction ) or ( q `1 <> 0 & contradiction ) )

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:53, EUCLID:54;
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:87; :: 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 :: thesis: not |[(((q `1) / (q `2)) / (q `2)),(1 / (q `2))]| in {(0. (TOP-REAL 2))}

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:52;
then A6: 0 = (1 / (q `2)) * (q `2) by Th3;
q `2 <> 0 by A5;
hence contradiction by A6, XCMPLX_1:87; :: 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