let n be Nat; :: thesis: Tunit_ball n, TOP-REAL n are_homeomorphic

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

set U = Tunit_ball n;

set C = TOP-REAL n;

reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

set U = Tunit_ball n;

set C = TOP-REAL n;

per cases
( not n is empty or n is empty )
;

end;

suppose A1:
not n is empty
; :: thesis: Tunit_ball n, TOP-REAL n are_homeomorphic

defpred S_{1}[ Point of (Tunit_ball n), set ] means ex w being Point of (TOP-REAL n1) st

( w = $1 & $2 = (1 / (1 - (|.w.| * |.w.|))) * w );

A2: for u being Point of (Tunit_ball n) ex y being Point of (TOP-REAL n) st S_{1}[u,y]

A3: for x being Point of (Tunit_ball n) holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A2);

for a being Point of (Tunit_ball n)

for b being Point of (TOP-REAL n1) st a = b holds

f . a = (1 / (1 - (|.b.| * |.b.|))) * b

end;( w = $1 & $2 = (1 / (1 - (|.w.| * |.w.|))) * w );

A2: for u being Point of (Tunit_ball n) ex y being Point of (TOP-REAL n) st S

proof

consider f being Function of (Tunit_ball n),(TOP-REAL n) such that
let u be Point of (Tunit_ball n); :: thesis: ex y being Point of (TOP-REAL n) st S_{1}[u,y]

reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25;

set y = (1 / (1 - (|.v.| * |.v.|))) * v;

reconsider y = (1 / (1 - (|.v.| * |.v.|))) * v as Point of (TOP-REAL n) ;

take y ; :: thesis: S_{1}[u,y]

thus S_{1}[u,y]
; :: thesis: verum

end;reconsider v = u as Point of (TOP-REAL n1) by PRE_TOPC:25;

set y = (1 / (1 - (|.v.| * |.v.|))) * v;

reconsider y = (1 / (1 - (|.v.| * |.v.|))) * v as Point of (TOP-REAL n) ;

take y ; :: thesis: S

thus S

A3: for x being Point of (Tunit_ball n) holds S

for a being Point of (Tunit_ball n)

for b being Point of (TOP-REAL n1) st a = b holds

f . a = (1 / (1 - (|.b.| * |.b.|))) * b

proof

hence
Tunit_ball n, TOP-REAL n are_homeomorphic
by T_0TOPSP:def 1, A1, Th6; :: thesis: verum
let a be Point of (Tunit_ball n); :: thesis: for b being Point of (TOP-REAL n1) st a = b holds

f . a = (1 / (1 - (|.b.| * |.b.|))) * b

let b be Point of (TOP-REAL n1); :: thesis: ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b )

S_{1}[a,f . a]
by A3;

hence ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) ; :: thesis: verum

end;f . a = (1 / (1 - (|.b.| * |.b.|))) * b

let b be Point of (TOP-REAL n1); :: thesis: ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b )

S

hence ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) ; :: thesis: verum

suppose A4:
n is empty
; :: thesis: Tunit_ball n, TOP-REAL n are_homeomorphic

A5:
for x being object holds

( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) )

.= Ball ((0. (TOP-REAL 0)),1) by A5, TARSKI:def 1 ;

hence Tunit_ball n, TOP-REAL n are_homeomorphic by A4, MFOLD_0:1; :: thesis: verum

end;( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) )

proof

[#] (TOP-REAL 0) =
{(0. (TOP-REAL 0))}
by EUCLID:22, EUCLID:77
let x be object ; :: thesis: ( x in Ball ((0. (TOP-REAL 0)),1) iff x = 0. (TOP-REAL 0) )

thus ( x in Ball ((0. (TOP-REAL 0)),1) implies x = 0. (TOP-REAL 0) ) ; :: thesis: ( x = 0. (TOP-REAL 0) implies x in Ball ((0. (TOP-REAL 0)),1) )

assume x = 0. (TOP-REAL 0) ; :: thesis: x in Ball ((0. (TOP-REAL 0)),1)

then reconsider p = x as Point of (TOP-REAL 0) ;

|.(p - (0. (TOP-REAL 0))).| < 1 by EUCLID_2:39;

hence x in Ball ((0. (TOP-REAL 0)),1) ; :: thesis: verum

end;thus ( x in Ball ((0. (TOP-REAL 0)),1) implies x = 0. (TOP-REAL 0) ) ; :: thesis: ( x = 0. (TOP-REAL 0) implies x in Ball ((0. (TOP-REAL 0)),1) )

assume x = 0. (TOP-REAL 0) ; :: thesis: x in Ball ((0. (TOP-REAL 0)),1)

then reconsider p = x as Point of (TOP-REAL 0) ;

|.(p - (0. (TOP-REAL 0))).| < 1 by EUCLID_2:39;

hence x in Ball ((0. (TOP-REAL 0)),1) ; :: thesis: verum

.= Ball ((0. (TOP-REAL 0)),1) by A5, TARSKI:def 1 ;

hence Tunit_ball n, TOP-REAL n are_homeomorphic by A4, MFOLD_0:1; :: thesis: verum