reconsider BP = NonZero (TOP-REAL 2) as non empty set by Th9;
defpred S1[ 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 S1[x,y]
ex h being Function of BP,BP st
for x being Element of BP holds S1[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))]| ) )
hence
ex b1 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 b1 . 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 b1 . p = |[(((p `1) / (p `2)) / (p `2)),(1 / (p `2))]| ) )
; verum