let h1, h2 be Function of (NonZero (TOP-REAL 2)),(NonZero (TOP-REAL 2)); :: thesis: ( ( 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 h1 . 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 h1 . p = |[(((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 h2 . 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 h2 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ) implies h1 = h2 )
assume that
A8: 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 h1 . 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 h1 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) and
A9: 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 h2 . 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 h2 . p = |[(((p `1 ) / (p `2 )) / (p `2 )),(1 / (p `2 ))]| ) ) ; :: thesis: h1 = h2
for x being set st x in NonZero (TOP-REAL 2) holds
h1 . x = h2 . x

proof

let x be set ; :: thesis: ( x in NonZero (TOP-REAL 2) implies h1 . x = h2 . x )
assume A10: x in NonZero (TOP-REAL 2) ; :: thesis: h1 . x = h2 . x
then reconsider q = x as Point of (TOP-REAL 2) ;
not q in {(0. (TOP-REAL 2))} by A10, XBOOLE_0:def 5;
then A11: q <> 0. (TOP-REAL 2) by TARSKI:def 1;

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 A12: ( ( q `2 <= q `1 & - (q `1 ) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: h1 . x = h2 . x

then h1 . q = |[(1 / (q `1 )),(((q `2 ) / (q `1 )) / (q `1 ))]| by A8, A11;
hence h1 . x = h2 . x by A9, A11, A12; :: thesis: verum

end;

case A13: ( not ( q `2 <= q `1 & - (q `1 ) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1 ) ) ) ; :: thesis: h1 . x = h2 . x

then h1 . q = |[(((q `1 ) / (q `2 )) / (q `2 )),(1 / (q `2 ))]| by A8, A11;
hence h1 . x = h2 . x by A9, A11, A13; :: thesis: verum

end;

end;

end;

hence h1 . x = h2 . x ; :: thesis: verum

end;

hence h1 = h2 by FUNCT_2:18; :: thesis: verum