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 object st x in NonZero (TOP-REAL 2) holds
h1 . x = h2 . x

proof

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

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:12; :: thesis: verum