let h1, h2 be Function of the carrier of (TOP-REAL 2), the carrier of (TOP-REAL 2); :: thesis: ( ( for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies h1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h1 . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h1 . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) ) & ( for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies h2 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h2 . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h2 . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) ) implies h1 = h2 )
assume that
A5: for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies h1 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h1 . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h1 . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) and
A6: for p being Point of (TOP-REAL 2) holds
( ( p = 0. (TOP-REAL 2) implies h2 . p = p ) & ( ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) ) & p <> 0. (TOP-REAL 2) implies h2 . p = |[((p `1) / (sqrt (1 + (((p `2) / (p `1)) ^2)))),((p `2) / (sqrt (1 + (((p `2) / (p `1)) ^2))))]| ) & ( ( p `2 <= p `1 & - (p `1) <= p `2 ) or ( p `2 >= p `1 & p `2 <= - (p `1) ) or not p <> 0. (TOP-REAL 2) or h2 . p = |[((p `1) / (sqrt (1 + (((p `1) / (p `2)) ^2)))),((p `2) / (sqrt (1 + (((p `1) / (p `2)) ^2))))]| ) ) ; :: thesis: h1 = h2
for x being object st x in the carrier of (TOP-REAL 2) holds
h1 . x = h2 . x

proof

let x be object ; :: thesis: ( x in the carrier of (TOP-REAL 2) implies h1 . x = h2 . x )
assume x in the carrier of (TOP-REAL 2) ; :: thesis: h1 . x = h2 . x
then reconsider q = x as Point of (TOP-REAL 2) ;

per cases ( q = 0. (TOP-REAL 2) or ( ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) & q <> 0. (TOP-REAL 2) ) or ( not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) & q <> 0. (TOP-REAL 2) ) ) ;

suppose A7: q = 0. (TOP-REAL 2) ; :: thesis: h1 . x = h2 . x

then h1 . q = q by A5;
hence h1 . x = h2 . x by A6, A7; :: thesis: verum

end;

suppose A8: ( ( ( q `2 <= q `1 & - (q `1) <= q `2 ) or ( q `2 >= q `1 & q `2 <= - (q `1) ) ) & q <> 0. (TOP-REAL 2) ) ; :: thesis: h1 . x = h2 . x

then h1 . q = |[((q `1) / (sqrt (1 + (((q `2) / (q `1)) ^2)))),((q `2) / (sqrt (1 + (((q `2) / (q `1)) ^2))))]| by A5;
hence h1 . x = h2 . x by A6, A8; :: thesis: verum

end;

suppose A9: ( not ( q `2 <= q `1 & - (q `1) <= q `2 ) & not ( q `2 >= q `1 & q `2 <= - (q `1) ) & q <> 0. (TOP-REAL 2) ) ; :: thesis: h1 . x = h2 . x

then h1 . q = |[((q `1) / (sqrt (1 + (((q `1) / (q `2)) ^2)))),((q `2) / (sqrt (1 + (((q `1) / (q `2)) ^2))))]| by A5;
hence h1 . x = h2 . x by A6, A9; :: thesis: verum

end;

end;

end;

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