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;

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

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

defpred S₁[ 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₁[u,y]

proof

let u be Point of (Tunit_ball n); :: thesis: ex y being Point of (TOP-REAL n) st S₁[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₁[u,y]
thus S₁[u,y] ; :: thesis: verum

end;

consider f being Function of (Tunit_ball n),(TOP-REAL n) such that
A3: for x being Point of (Tunit_ball n) holds S₁[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

proof

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₁[a,f . a] by A3;
hence ( a = b implies f . a = (1 / (1 - (|.b.| * |.b.|))) * b ) ; :: thesis: verum

end;

hence Tunit_ball n, TOP-REAL n are_homeomorphic by T_0TOPSP:def 1, A1, Th6; :: thesis: verum

end;

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) )

proof

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;

[#] (TOP-REAL 0) = {(0. (TOP-REAL 0))} by EUCLID:22, EUCLID:77
.= 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;

end;