let h1, h2 be Function of the carrier of (TOP-REAL 2) \ {(0.REAL 2)},the carrier of (TOP-REAL 2) \ {(0.REAL 2)}; :: thesis: ( ( 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 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.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 A8: ( ( 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 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.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 the carrier of (TOP-REAL 2) \ {(0.REAL 2)} holds
h1 . x = h2 . x

proof

let x be set ; :: thesis: ( x in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} implies h1 . x = h2 . x )
assume A9: x in the carrier of (TOP-REAL 2) \ {(0.REAL 2)} ; :: thesis: h1 . x = h2 . x
then reconsider q = x as Point of (TOP-REAL 2) ;
not q in {(0.REAL 2)} by A9, XBOOLE_0:def 5;
then A10: q <> 0.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 A11: ( ( 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, A10;
hence h1 . x = h2 . x by A8, A10, A11; :: thesis: verum

end;

case A12: ( 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, A10;
hence h1 . x = h2 . x by A8, A10, A12; :: thesis: verum

end;

end;

end;

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

end;

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