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 set st x in the carrier of (TOP-REAL 2) holds
h1 . x = h2 . x

proof

let x be set ; :: 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:18; :: thesis: verum