let N be non zero Nat; :: thesis: for F being Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)) st ( for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ) holds

( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

set N1 = N + 1;

set Tn1 = TOP-REAL (N + 1);

set Tn = TOP-REAL N;

N: N in NAT by ORDINAL1:def 12;

set N0 = (0* (N + 1)) +* ((N + 1),(- 1));

A1: len ((0* (N + 1)) +* ((N + 1),(- 1))) = N + 1 by CARD_1:def 7;

rng ((0* (N + 1)) +* ((N + 1),(- 1))) c= REAL ;

then (0* (N + 1)) +* ((N + 1),(- 1)) is FinSequence of REAL by FINSEQ_1:def 4;

then reconsider N0 = (0* (N + 1)) +* ((N + 1),(- 1)) as Point of (TOP-REAL (N + 1)) by A1, TOPREAL7:17;

set NF = N NormF ;

set NNF = (N NormF) (#) (N NormF);

reconsider ONE = 1 as Element of NAT ;

set TD = Tdisk ((0. (TOP-REAL N)),1);

A2: [#] (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by PRE_TOPC:def 5;

reconsider NNF = (N NormF) (#) (N NormF) as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider mNNF = - NNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider m1 = 1 + mNNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

1 <= N + 1 by NAT_1:11;

then A3: N + 1 in Seg (N + 1) ;

dom (0* (N + 1)) = Seg (N + 1) ;

then A4: N0 . (N + 1) = - 1 by A3, FUNCT_7:31;

let F be Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)); :: thesis: ( ( for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ) implies ( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) ) )

set FF = <:F:>;

A5: N < N + 1 by NAT_1:13;

len F = N by CARD_1:def 7;

then A6: dom F = Seg N by FINSEQ_1:def 3;

assume A7: for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ; :: thesis: ( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

thus A8: for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N :: thesis: for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) )

assume A17: Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } ; :: thesis: ( not Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } or ( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) )

A18: dom <:F:> = the carrier of (TOP-REAL (N + 1)) by FUNCT_2:def 1;

A19: cl_Ball ((0. (TOP-REAL N)),1) c= <:F:> .: Sp

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

A29: cl_Ball ((0. (TOP-REAL N)),1) c= <:F:> .: Sn

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

A54: <:F:> .: Sn c= cl_Ball ((0. (TOP-REAL N)),1)

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

<:F:> .: (Sn /\ Sp) c= Sphere ((0. (TOP-REAL N)),1)

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

thus for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism :: thesis: for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism

assume A139: H = <:F:> | Sn ; :: thesis: H is being_homeomorphism

A140: dom H = [#] ((TOP-REAL (N + 1)) | Sn) by FUNCT_2:def 1;

A141: [#] ((TOP-REAL (N + 1)) | Sn) = Sn by PRE_TOPC:def 5;

then A142: rng H = (<:F:> | Sn) .: Sn by A140, A139, RELAT_1:113

.= cl_Ball ((0. (TOP-REAL N)),1) by A29, A54, RELAT_1:129 ;

then A143: rng H = [#] (Tdisk ((0. (TOP-REAL N)),1)) by PRE_TOPC:def 5;

A144: for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds

x1 = x2

set TD = Tdisk ((0. (TOP-REAL N)),1);

set M = m1 | (Tdisk ((0. (TOP-REAL N)),1));

A161: dom (m1 | (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

reconsider MM = m1 | (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL by TOPMETR:17, JORDAN5A:27;

reconsider Msqr = - (sqrt MM) as Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL ;

A162: m1 | (Tdisk ((0. (TOP-REAL N)),1)) = m1 | the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by TMAP_1:def 4;

A163: for p being Point of (TOP-REAL N) st p in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) holds

MM . p = 1 - (|.p.| * |.p.|)

then reconsider SQR = |[Msqr]| as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL 1) ;

A168: dom (sqrt MM) = dom MM by PARTFUN3:def 5;

A169: rng (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

dom (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

then reconsider ID = id (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL N) by A169, FUNCT_2:2, A164, PRE_TOPC:26;

reconsider SQR = SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL ONE) ;

reconsider II = ID ^^ SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + ONE)) ;

reconsider II = II as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + 1)) ;

A170: dom II = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

dom (- (sqrt MM)) = dom (sqrt MM) by VALUED_1:8;

then A171: dom SQR = dom (sqrt MM) by Def1;

for y, x being object holds

( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

|.N0.| = |.(- 1).| by TOPREALC:13, A3

.= - (- 1) by ABSVALUE:def 1 ;

then A199: N0 in Sn by A28, A4;

for P being Subset of ((TOP-REAL (N + 1)) | Sn) holds

( P is open iff H .: P is open )

F . i = PROJ ((N + 1),i) ) holds

( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

set N1 = N + 1;

set Tn1 = TOP-REAL (N + 1);

set Tn = TOP-REAL N;

N: N in NAT by ORDINAL1:def 12;

set N0 = (0* (N + 1)) +* ((N + 1),(- 1));

A1: len ((0* (N + 1)) +* ((N + 1),(- 1))) = N + 1 by CARD_1:def 7;

rng ((0* (N + 1)) +* ((N + 1),(- 1))) c= REAL ;

then (0* (N + 1)) +* ((N + 1),(- 1)) is FinSequence of REAL by FINSEQ_1:def 4;

then reconsider N0 = (0* (N + 1)) +* ((N + 1),(- 1)) as Point of (TOP-REAL (N + 1)) by A1, TOPREAL7:17;

set NF = N NormF ;

set NNF = (N NormF) (#) (N NormF);

reconsider ONE = 1 as Element of NAT ;

set TD = Tdisk ((0. (TOP-REAL N)),1);

A2: [#] (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by PRE_TOPC:def 5;

reconsider NNF = (N NormF) (#) (N NormF) as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider mNNF = - NNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider m1 = 1 + mNNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

1 <= N + 1 by NAT_1:11;

then A3: N + 1 in Seg (N + 1) ;

dom (0* (N + 1)) = Seg (N + 1) ;

then A4: N0 . (N + 1) = - 1 by A3, FUNCT_7:31;

let F be Element of N -tuples_on (Funcs ( the carrier of (TOP-REAL (N + 1)), the carrier of R^1)); :: thesis: ( ( for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ) implies ( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) ) )

set FF = <:F:>;

A5: N < N + 1 by NAT_1:13;

len F = N by CARD_1:def 7;

then A6: dom F = Seg N by FINSEQ_1:def 3;

assume A7: for i being Nat st i in dom F holds

F . i = PROJ ((N + 1),i) ; :: thesis: ( ( for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N ) & ( for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) ) )

thus A8: for t being Point of (TOP-REAL (N + 1)) holds <:F:> . t = t | N :: thesis: for Sp, Sn being Subset of (TOP-REAL (N + 1)) st Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } holds

( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

proof

let Sp, Sn be Subset of (TOP-REAL (N + 1)); :: thesis: ( Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } & Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } implies ( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
let s be Point of (TOP-REAL (N + 1)); :: thesis: <:F:> . s = s | N

reconsider Fs = <:F:> . s as Point of (TOP-REAL N) ;

A9: len Fs = N by CARD_1:def 7;

A10: len s = N + 1 by CARD_1:def 7;

end;reconsider Fs = <:F:> . s as Point of (TOP-REAL N) ;

A9: len Fs = N by CARD_1:def 7;

A10: len s = N + 1 by CARD_1:def 7;

now :: thesis: for i being Nat st 1 <= i & i <= N holds

Fs . i = (s | N) . i

hence
<:F:> . s = s | N
by A9, A10, FINSEQ_1:59, A5; :: thesis: verumFs . i = (s | N) . i

let i be Nat; :: thesis: ( 1 <= i & i <= N implies Fs . i = (s | N) . i )

assume that

A12: 1 <= i and

A13: i <= N ; :: thesis: Fs . i = (s | N) . i

A14: Fs . i = (F . i) . s by TIETZE_2:1;

i < N + 1 by A13, NAT_1:13;

then A15: i in dom s by A10, A12, FINSEQ_3:25;

F . i = PROJ ((N + 1),i) by A12, A13, FINSEQ_1:1, A7, A6;

then A16: Fs . i = s /. i by A14, TOPREALC:def 6;

(s | N) . i = s . i by A12, A13, FINSEQ_1:1, FUNCT_1:49;

hence Fs . i = (s | N) . i by A16, A15, PARTFUN1:def 6; :: thesis: verum

end;assume that

A12: 1 <= i and

A13: i <= N ; :: thesis: Fs . i = (s | N) . i

A14: Fs . i = (F . i) . s by TIETZE_2:1;

i < N + 1 by A13, NAT_1:13;

then A15: i in dom s by A10, A12, FINSEQ_3:25;

F . i = PROJ ((N + 1),i) by A12, A13, FINSEQ_1:1, A7, A6;

then A16: Fs . i = s /. i by A14, TOPREALC:def 6;

(s | N) . i = s . i by A12, A13, FINSEQ_1:1, FUNCT_1:49;

hence Fs . i = (s | N) . i by A16, A15, PARTFUN1:def 6; :: thesis: verum

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) )

assume A17: Sp = { u where u is Point of (TOP-REAL (N + 1)) : ( u . (N + 1) >= 0 & |.u.| = 1 ) } ; :: thesis: ( not Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) } or ( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) ) )

A18: dom <:F:> = the carrier of (TOP-REAL (N + 1)) by FUNCT_2:def 1;

A19: cl_Ball ((0. (TOP-REAL N)),1) c= <:F:> .: Sp

proof

assume A28:
Sn = { t where t is Point of (TOP-REAL (N + 1)) : ( t . (N + 1) <= 0 & |.t.| = 1 ) }
; :: thesis: ( <:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball ((0. (TOP-REAL N)),1) or x in <:F:> .: Sp )

assume A20: x in cl_Ball ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: Sp

then reconsider s = x as Element of REAL N by EUCLID:22;

set sq = sqrt (1 - (|.s.| ^2));

set s1 = s ^ <*(sqrt (1 - (|.s.| ^2)))*>;

|.s.| <= 1 by TOPREAL9:11, A20;

then |.s.| * |.s.| <= 1 * 1 by XREAL_1:66;

then A21: 1 - (|.s.| ^2) >= (|.s.| ^2) - (|.s.| ^2) by XREAL_1:13;

then A22: (sqrt (1 - (|.s.| ^2))) ^2 = 1 - (|.s.| ^2) by SQUARE_1:def 2;

A23: len (s ^ <*(sqrt (1 - (|.s.| ^2)))*>) = (len s) + 1 by FINSEQ_2:16;

A24: len s = N by CARD_1:def 7;

s ^ <*(sqrt (1 - (|.s.| ^2)))*> is FinSequence of REAL by RVSUM_1:145;

then reconsider s1 = s ^ <*(sqrt (1 - (|.s.| ^2)))*> as Element of REAL (N + 1) by A23, A24, FINSEQ_2:92;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A23, CARD_1:def 7;

then A25: s1 | N = s by FINSEQ_2:17;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

A26: s1 . (N + 1) = sqrt (1 - (|.s.| ^2)) by A24, FINSEQ_1:42;

then |.s1.| ^2 = (|.s.| ^2) + ((sqrt (1 - (|.s.| ^2))) ^2) by A25, REAL_NS1:10

.= 1 ^2 by A22 ;

then ( |.s1.| = 1 or |.s1.| = - 1 ) by SQUARE_1:40;

then A27: ss1 in Sp by A17, A26, A21;

<:F:> . ss1 = s by A25, A8;

hence x in <:F:> .: Sp by A27, A18, FUNCT_1:def 6; :: thesis: verum

end;assume A20: x in cl_Ball ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: Sp

then reconsider s = x as Element of REAL N by EUCLID:22;

set sq = sqrt (1 - (|.s.| ^2));

set s1 = s ^ <*(sqrt (1 - (|.s.| ^2)))*>;

|.s.| <= 1 by TOPREAL9:11, A20;

then |.s.| * |.s.| <= 1 * 1 by XREAL_1:66;

then A21: 1 - (|.s.| ^2) >= (|.s.| ^2) - (|.s.| ^2) by XREAL_1:13;

then A22: (sqrt (1 - (|.s.| ^2))) ^2 = 1 - (|.s.| ^2) by SQUARE_1:def 2;

A23: len (s ^ <*(sqrt (1 - (|.s.| ^2)))*>) = (len s) + 1 by FINSEQ_2:16;

A24: len s = N by CARD_1:def 7;

s ^ <*(sqrt (1 - (|.s.| ^2)))*> is FinSequence of REAL by RVSUM_1:145;

then reconsider s1 = s ^ <*(sqrt (1 - (|.s.| ^2)))*> as Element of REAL (N + 1) by A23, A24, FINSEQ_2:92;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A23, CARD_1:def 7;

then A25: s1 | N = s by FINSEQ_2:17;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

A26: s1 . (N + 1) = sqrt (1 - (|.s.| ^2)) by A24, FINSEQ_1:42;

then |.s1.| ^2 = (|.s.| ^2) + ((sqrt (1 - (|.s.| ^2))) ^2) by A25, REAL_NS1:10

.= 1 ^2 by A22 ;

then ( |.s1.| = 1 or |.s1.| = - 1 ) by SQUARE_1:40;

then A27: ss1 in Sp by A17, A26, A21;

<:F:> . ss1 = s by A25, A8;

hence x in <:F:> .: Sp by A27, A18, FUNCT_1:def 6; :: thesis: verum

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

A29: cl_Ball ((0. (TOP-REAL N)),1) c= <:F:> .: Sn

proof

A38:
Sphere ((0. (TOP-REAL N)),1) c= <:F:> .: (Sn /\ Sp)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in cl_Ball ((0. (TOP-REAL N)),1) or x in <:F:> .: Sn )

assume A30: x in cl_Ball ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: Sn

then reconsider s = x as Element of REAL N by EUCLID:22;

|.s.| <= 1 by TOPREAL9:11, A30;

then |.s.| * |.s.| <= 1 * 1 by XREAL_1:66;

then A31: 1 - (|.s.| ^2) >= (|.s.| ^2) - (|.s.| ^2) by XREAL_1:13;

set sq = - (sqrt (1 - (|.s.| ^2)));

set s1 = s ^ <*(- (sqrt (1 - (|.s.| ^2))))*>;

A32: len (s ^ <*(- (sqrt (1 - (|.s.| ^2))))*>) = (len s) + 1 by FINSEQ_2:16;

(- (sqrt (1 - (|.s.| ^2)))) ^2 = (- (- (sqrt (1 - (|.s.| ^2))))) ^2 ;

then A33: (- (sqrt (1 - (|.s.| ^2)))) ^2 = 1 - (|.s.| ^2) by SQUARE_1:def 2, A31;

A34: len s = N by CARD_1:def 7;

s ^ <*(- (sqrt (1 - (|.s.| ^2))))*> is FinSequence of REAL by RVSUM_1:145;

then reconsider s1 = s ^ <*(- (sqrt (1 - (|.s.| ^2))))*> as Element of REAL (N + 1) by A32, A34, FINSEQ_2:92;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A32, CARD_1:def 7;

then A35: s1 | N = s by FINSEQ_2:17;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

A36: s1 . (N + 1) = - (sqrt (1 - (|.s.| ^2))) by A34, FINSEQ_1:42;

then |.s1.| ^2 = (|.s.| ^2) + ((- (sqrt (1 - (|.s.| ^2)))) ^2) by A35, REAL_NS1:10

.= 1 ^2 by A33 ;

then ( |.s1.| = 1 or |.s1.| = - 1 ) by SQUARE_1:40;

then A37: ss1 in Sn by A28, A36, A31;

<:F:> . ss1 = s by A35, A8;

hence x in <:F:> .: Sn by A37, A18, FUNCT_1:def 6; :: thesis: verum

end;assume A30: x in cl_Ball ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: Sn

then reconsider s = x as Element of REAL N by EUCLID:22;

|.s.| <= 1 by TOPREAL9:11, A30;

then |.s.| * |.s.| <= 1 * 1 by XREAL_1:66;

then A31: 1 - (|.s.| ^2) >= (|.s.| ^2) - (|.s.| ^2) by XREAL_1:13;

set sq = - (sqrt (1 - (|.s.| ^2)));

set s1 = s ^ <*(- (sqrt (1 - (|.s.| ^2))))*>;

A32: len (s ^ <*(- (sqrt (1 - (|.s.| ^2))))*>) = (len s) + 1 by FINSEQ_2:16;

(- (sqrt (1 - (|.s.| ^2)))) ^2 = (- (- (sqrt (1 - (|.s.| ^2))))) ^2 ;

then A33: (- (sqrt (1 - (|.s.| ^2)))) ^2 = 1 - (|.s.| ^2) by SQUARE_1:def 2, A31;

A34: len s = N by CARD_1:def 7;

s ^ <*(- (sqrt (1 - (|.s.| ^2))))*> is FinSequence of REAL by RVSUM_1:145;

then reconsider s1 = s ^ <*(- (sqrt (1 - (|.s.| ^2))))*> as Element of REAL (N + 1) by A32, A34, FINSEQ_2:92;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A32, CARD_1:def 7;

then A35: s1 | N = s by FINSEQ_2:17;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

A36: s1 . (N + 1) = - (sqrt (1 - (|.s.| ^2))) by A34, FINSEQ_1:42;

then |.s1.| ^2 = (|.s.| ^2) + ((- (sqrt (1 - (|.s.| ^2)))) ^2) by A35, REAL_NS1:10

.= 1 ^2 by A33 ;

then ( |.s1.| = 1 or |.s1.| = - 1 ) by SQUARE_1:40;

then A37: ss1 in Sn by A28, A36, A31;

<:F:> . ss1 = s by A35, A8;

hence x in <:F:> .: Sn by A37, A18, FUNCT_1:def 6; :: thesis: verum

proof

A48:
<:F:> .: Sp c= cl_Ball ((0. (TOP-REAL N)),1)
reconsider Z = 0 as Element of REAL by XREAL_0:def 1;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sphere ((0. (TOP-REAL N)),1) or x in <:F:> .: (Sn /\ Sp) )

assume A39: x in Sphere ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: (Sn /\ Sp)

then reconsider s = x as Element of REAL N by EUCLID:22;

A40: |.s.| = 1 by TOPREAL9:12, A39;

set s1 = s ^ <*Z*>;

A41: len s = N by CARD_1:def 7;

A42: len (s ^ <*Z*>) = (len s) + 1 by FINSEQ_2:16;

then reconsider s1 = s ^ <*Z*> as Element of REAL (N + 1) by A41, FINSEQ_2:92;

A43: s1 . (N + 1) = 0 by A41, FINSEQ_1:42;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A42, CARD_1:def 7;

then A44: s1 | N = s by FINSEQ_2:17;

then |.s1.| ^2 = (|.s.| ^2) + (0 ^2) by A43, REAL_NS1:10;

then A45: ( |.s1.| = 1 or |.s1.| = - 1 ) by A40, SQUARE_1:40;

then A46: ss1 in Sn by A28, A43;

ss1 in Sp by A45, A17, A43;

then A47: ss1 in Sp /\ Sn by A46, XBOOLE_0:def 4;

<:F:> . ss1 = s by A44, A8;

hence x in <:F:> .: (Sn /\ Sp) by A47, A18, FUNCT_1:def 6; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sphere ((0. (TOP-REAL N)),1) or x in <:F:> .: (Sn /\ Sp) )

assume A39: x in Sphere ((0. (TOP-REAL N)),1) ; :: thesis: x in <:F:> .: (Sn /\ Sp)

then reconsider s = x as Element of REAL N by EUCLID:22;

A40: |.s.| = 1 by TOPREAL9:12, A39;

set s1 = s ^ <*Z*>;

A41: len s = N by CARD_1:def 7;

A42: len (s ^ <*Z*>) = (len s) + 1 by FINSEQ_2:16;

then reconsider s1 = s ^ <*Z*> as Element of REAL (N + 1) by A41, FINSEQ_2:92;

A43: s1 . (N + 1) = 0 by A41, FINSEQ_1:42;

reconsider ss1 = s1 as Point of (TOP-REAL (N + 1)) by EUCLID:22;

(s1 | N) ^ <*(s1 . (N + 1))*> = s1 by FINSEQ_3:55, A42, CARD_1:def 7;

then A44: s1 | N = s by FINSEQ_2:17;

then |.s1.| ^2 = (|.s.| ^2) + (0 ^2) by A43, REAL_NS1:10;

then A45: ( |.s1.| = 1 or |.s1.| = - 1 ) by A40, SQUARE_1:40;

then A46: ss1 in Sn by A28, A43;

ss1 in Sp by A45, A17, A43;

then A47: ss1 in Sp /\ Sn by A46, XBOOLE_0:def 4;

<:F:> . ss1 = s by A44, A8;

hence x in <:F:> .: (Sn /\ Sp) by A47, A18, FUNCT_1:def 6; :: thesis: verum

proof

hence
<:F:> .: Sp = cl_Ball ((0. (TOP-REAL N)),1)
by A19; :: thesis: ( <:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1) & <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:F:> .: Sp or y in cl_Ball ((0. (TOP-REAL N)),1) )

assume y in <:F:> .: Sp ; :: thesis: y in cl_Ball ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A49: x in Sp and

A50: <:F:> . x = y by FUNCT_1:def 6;

consider s being Point of (TOP-REAL (N + 1)) such that

A51: s = x and

s . (N + 1) >= 0 and

A52: |.s.| = 1 by A49, A17;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

|.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

then |.ss.| ^2 >= (|.sN.| ^2) + 0 by XREAL_1:6;

then A53: 1 >= |.sN.| by SQUARE_1:16, A52;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in cl_Ball ((0. (TOP-REAL N)),1) by A53;

hence y in cl_Ball ((0. (TOP-REAL N)),1) by A8, A51, A50; :: thesis: verum

end;assume y in <:F:> .: Sp ; :: thesis: y in cl_Ball ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A49: x in Sp and

A50: <:F:> . x = y by FUNCT_1:def 6;

consider s being Point of (TOP-REAL (N + 1)) such that

A51: s = x and

s . (N + 1) >= 0 and

A52: |.s.| = 1 by A49, A17;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

|.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

then |.ss.| ^2 >= (|.sN.| ^2) + 0 by XREAL_1:6;

then A53: 1 >= |.sN.| by SQUARE_1:16, A52;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in cl_Ball ((0. (TOP-REAL N)),1) by A53;

hence y in cl_Ball ((0. (TOP-REAL N)),1) by A8, A51, A50; :: thesis: verum

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

A54: <:F:> .: Sn c= cl_Ball ((0. (TOP-REAL N)),1)

proof

hence
<:F:> .: Sn = cl_Ball ((0. (TOP-REAL N)),1)
by A29; :: thesis: ( <:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1) & ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:F:> .: Sn or y in cl_Ball ((0. (TOP-REAL N)),1) )

assume y in <:F:> .: Sn ; :: thesis: y in cl_Ball ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A55: x in Sn and

A56: <:F:> . x = y by FUNCT_1:def 6;

consider s being Point of (TOP-REAL (N + 1)) such that

A57: s = x and

s . (N + 1) <= 0 and

A58: |.s.| = 1 by A55, A28;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

|.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

then |.ss.| ^2 >= (|.sN.| ^2) + 0 by XREAL_1:6;

then A59: 1 >= |.sN.| by SQUARE_1:16, A58;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in cl_Ball ((0. (TOP-REAL N)),1) by A59;

hence y in cl_Ball ((0. (TOP-REAL N)),1) by A8, A57, A56; :: thesis: verum

end;assume y in <:F:> .: Sn ; :: thesis: y in cl_Ball ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A55: x in Sn and

A56: <:F:> . x = y by FUNCT_1:def 6;

consider s being Point of (TOP-REAL (N + 1)) such that

A57: s = x and

s . (N + 1) <= 0 and

A58: |.s.| = 1 by A55, A28;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

|.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

then |.ss.| ^2 >= (|.sN.| ^2) + 0 by XREAL_1:6;

then A59: 1 >= |.sN.| by SQUARE_1:16, A58;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in cl_Ball ((0. (TOP-REAL N)),1) by A59;

hence y in cl_Ball ((0. (TOP-REAL N)),1) by A8, A57, A56; :: thesis: verum

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

<:F:> .: (Sn /\ Sp) c= Sphere ((0. (TOP-REAL N)),1)

proof

hence
<:F:> .: (Sp /\ Sn) = Sphere ((0. (TOP-REAL N)),1)
by A38; :: thesis: ( ( for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in <:F:> .: (Sn /\ Sp) or y in Sphere ((0. (TOP-REAL N)),1) )

assume y in <:F:> .: (Sn /\ Sp) ; :: thesis: y in Sphere ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A60: x in Sn /\ Sp and

A61: <:F:> . x = y by FUNCT_1:def 6;

x in Sn by A60, XBOOLE_0:def 4;

then consider s being Point of (TOP-REAL (N + 1)) such that

A62: s = x and

A63: s . (N + 1) <= 0 and

A64: |.s.| = 1 by A28;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

A65: |.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

x in Sp by A60, XBOOLE_0:def 4;

then ex s1 being Point of (TOP-REAL (N + 1)) st

( s1 = x & s1 . (N + 1) >= 0 & |.s1.| = 1 ) by A17;

then (s . (N + 1)) ^2 = 0 by A62, A63;

then A66: ( |.ss.| = |.sN.| or |.ss.| = - |.sN.| ) by A65, SQUARE_1:40;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in Sphere ((0. (TOP-REAL N)),1) by A66, A64;

hence y in Sphere ((0. (TOP-REAL N)),1) by A8, A62, A61; :: thesis: verum

end;assume y in <:F:> .: (Sn /\ Sp) ; :: thesis: y in Sphere ((0. (TOP-REAL N)),1)

then consider x being object such that

x in dom <:F:> and

A60: x in Sn /\ Sp and

A61: <:F:> . x = y by FUNCT_1:def 6;

x in Sn by A60, XBOOLE_0:def 4;

then consider s being Point of (TOP-REAL (N + 1)) such that

A62: s = x and

A63: s . (N + 1) <= 0 and

A64: |.s.| = 1 by A28;

reconsider ss = s as Element of REAL (N + 1) by EUCLID:22;

len ss = N + 1 by CARD_1:def 7;

then len (ss | N) = N by A5, FINSEQ_1:59;

then reconsider sN = ss | N as Point of (TOP-REAL N) by TOPREAL7:17;

A65: |.ss.| ^2 = (|.sN.| ^2) + ((s . (N + 1)) ^2) by REAL_NS1:10;

x in Sp by A60, XBOOLE_0:def 4;

then ex s1 being Point of (TOP-REAL (N + 1)) st

( s1 = x & s1 . (N + 1) >= 0 & |.s1.| = 1 ) by A17;

then (s . (N + 1)) ^2 = 0 by A62, A63;

then A66: ( |.ss.| = |.sN.| or |.ss.| = - |.sN.| ) by A65, SQUARE_1:40;

sN - (0. (TOP-REAL N)) = sN by RLVECT_1:13;

then sN in Sphere ((0. (TOP-REAL N)),1) by A66, A64;

hence y in Sphere ((0. (TOP-REAL N)),1) by A8, A62, A61; :: thesis: verum

H is being_homeomorphism ) & ( for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism ) )

thus for H being Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sp holds

H is being_homeomorphism :: thesis: for H being Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)) st H = <:F:> | Sn holds

H is being_homeomorphism

proof

let H be Function of ((TOP-REAL (N + 1)) | Sn),(Tdisk ((0. (TOP-REAL N)),1)); :: thesis: ( H = <:F:> | Sn implies H is being_homeomorphism )
set N0 = (0* (N + 1)) +* ((N + 1),1);

rng ((0* (N + 1)) +* ((N + 1),1)) c= REAL ;

then W: (0* (N + 1)) +* ((N + 1),1) is FinSequence of REAL by FINSEQ_1:def 4;

len ((0* (N + 1)) +* ((N + 1),1)) = N + 1 by CARD_1:def 7;

then reconsider N0 = (0* (N + 1)) +* ((N + 1),1) as Point of (TOP-REAL (N + 1)) by W, TOPREAL7:17;

reconsider ONE = 1 as Element of NAT ;

set NF = N NormF ;

set NNF = (N NormF) (#) (N NormF);

A67: [#] (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by PRE_TOPC:def 5;

reconsider NNF = (N NormF) (#) (N NormF) as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider mNNF = - NNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider m1 = 1 + mNNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

1 <= N + 1 by NAT_1:11;

then A68: N + 1 in Seg (N + 1) ;

then A69: |.N0.| = |.1.| by TOPREALC:13

.= 1 by ABSVALUE:def 1 ;

let H be Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)); :: thesis: ( H = <:F:> | Sp implies H is being_homeomorphism )

assume A70: H = <:F:> | Sp ; :: thesis: H is being_homeomorphism

A71: dom H = [#] ((TOP-REAL (N + 1)) | Sp) by FUNCT_2:def 1;

A72: [#] ((TOP-REAL (N + 1)) | Sp) = Sp by PRE_TOPC:def 5;

then A73: rng H = (<:F:> | Sp) .: Sp by A71, A70, RELAT_1:113

.= cl_Ball ((0. (TOP-REAL N)),1) by A19, A48, RELAT_1:129 ;

then A74: rng H = [#] (Tdisk ((0. (TOP-REAL N)),1)) by PRE_TOPC:def 5;

A75: for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds

x1 = x2

set TD = Tdisk ((0. (TOP-REAL N)),1);

set M = m1 | (Tdisk ((0. (TOP-REAL N)),1));

A92: dom (m1 | (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

reconsider MM = m1 | (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL by TOPMETR:17, JORDAN5A:27;

A93: m1 | (Tdisk ((0. (TOP-REAL N)),1)) = m1 | the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by TMAP_1:def 4;

A94: for p being Point of (TOP-REAL N) st p in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) holds

MM . p = 1 - (|.p.| * |.p.|)

then reconsider SQR = |[(sqrt MM)]| as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL 1) ;

A99: dom (sqrt MM) = dom MM by PARTFUN3:def 5;

A100: rng (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

dom (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

then reconsider ID = id (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL N) by A100, FUNCT_2:2, A95, PRE_TOPC:26;

reconsider SQR = SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL ONE) ;

reconsider II = ID ^^ SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + ONE)) ;

reconsider II = II as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + 1)) ;

A101: dom II = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

A102: dom SQR = dom (sqrt MM) by Def1;

for y, x being object holds

( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

dom (0* (N + 1)) = Seg (N + 1) ;

then N0 . (N + 1) = 1 by A68, FUNCT_7:31;

then A129: N0 in Sp by A69, A17;

for P being Subset of ((TOP-REAL (N + 1)) | Sp) holds

( P is open iff H .: P is open )

end;rng ((0* (N + 1)) +* ((N + 1),1)) c= REAL ;

then W: (0* (N + 1)) +* ((N + 1),1) is FinSequence of REAL by FINSEQ_1:def 4;

len ((0* (N + 1)) +* ((N + 1),1)) = N + 1 by CARD_1:def 7;

then reconsider N0 = (0* (N + 1)) +* ((N + 1),1) as Point of (TOP-REAL (N + 1)) by W, TOPREAL7:17;

reconsider ONE = 1 as Element of NAT ;

set NF = N NormF ;

set NNF = (N NormF) (#) (N NormF);

A67: [#] (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by PRE_TOPC:def 5;

reconsider NNF = (N NormF) (#) (N NormF) as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider mNNF = - NNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

reconsider m1 = 1 + mNNF as Function of (TOP-REAL N),R^1 by TOPMETR:17;

1 <= N + 1 by NAT_1:11;

then A68: N + 1 in Seg (N + 1) ;

then A69: |.N0.| = |.1.| by TOPREALC:13

.= 1 by ABSVALUE:def 1 ;

let H be Function of ((TOP-REAL (N + 1)) | Sp),(Tdisk ((0. (TOP-REAL N)),1)); :: thesis: ( H = <:F:> | Sp implies H is being_homeomorphism )

assume A70: H = <:F:> | Sp ; :: thesis: H is being_homeomorphism

A71: dom H = [#] ((TOP-REAL (N + 1)) | Sp) by FUNCT_2:def 1;

A72: [#] ((TOP-REAL (N + 1)) | Sp) = Sp by PRE_TOPC:def 5;

then A73: rng H = (<:F:> | Sp) .: Sp by A71, A70, RELAT_1:113

.= cl_Ball ((0. (TOP-REAL N)),1) by A19, A48, RELAT_1:129 ;

then A74: rng H = [#] (Tdisk ((0. (TOP-REAL N)),1)) by PRE_TOPC:def 5;

A75: for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds

x1 = x2

proof

then A91:
H is one-to-one
;
let x1, x2 be object ; :: thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )

assume A76: x1 in dom H ; :: thesis: ( not x2 in dom H or not H . x1 = H . x2 or x1 = x2 )

then consider s1 being Point of (TOP-REAL (N + 1)) such that

A77: x1 = s1 and

A78: s1 . (N + 1) >= 0 and

A79: |.s1.| = 1 by A17, A71, A72;

assume A80: x2 in dom H ; :: thesis: ( not H . x1 = H . x2 or x1 = x2 )

then consider s2 being Point of (TOP-REAL (N + 1)) such that

A81: x2 = s2 and

A82: s2 . (N + 1) >= 0 and

A83: |.s2.| = 1 by A17, A71, A72;

reconsider s1 = s1, s2 = s2 as Element of REAL (N + 1) by EUCLID:22;

A84: 1 ^2 = (|.(s1 | N).| ^2) + ((s1 . (N + 1)) ^2) by REAL_NS1:10, A79;

A85: H . x2 = <:F:> . x2 by A70, FUNCT_1:47, A80;

assume A86: H . x1 = H . x2 ; :: thesis: x1 = x2

H . x1 = <:F:> . x1 by A76, A70, FUNCT_1:47;

then A87: s1 | N = <:F:> . s2 by A85, A86, A8, A77, A81

.= s2 | N by A8 ;

then 1 ^2 = (|.(s1 | N).| ^2) + ((s2 . (N + 1)) ^2) by REAL_NS1:10, A83;

then A88: ( s1 . (N + 1) = s2 . (N + 1) or s1 . (N + 1) = - (s2 . (N + 1)) ) by A84, SQUARE_1:40;

A89: ( s1 . (N + 1) > 0 or s1 . (N + 1) = 0 ) by A78;

A90: len s2 = N + 1 by CARD_1:def 7;

len s1 = N + 1 by CARD_1:def 7;

hence x1 = (s1 | N) ^ <*(s1 . (N + 1))*> by FINSEQ_3:55, A77

.= x2 by FINSEQ_3:55, A88, A89, A82, A90, A87, A81 ;

:: thesis: verum

end;assume A76: x1 in dom H ; :: thesis: ( not x2 in dom H or not H . x1 = H . x2 or x1 = x2 )

then consider s1 being Point of (TOP-REAL (N + 1)) such that

A77: x1 = s1 and

A78: s1 . (N + 1) >= 0 and

A79: |.s1.| = 1 by A17, A71, A72;

assume A80: x2 in dom H ; :: thesis: ( not H . x1 = H . x2 or x1 = x2 )

then consider s2 being Point of (TOP-REAL (N + 1)) such that

A81: x2 = s2 and

A82: s2 . (N + 1) >= 0 and

A83: |.s2.| = 1 by A17, A71, A72;

reconsider s1 = s1, s2 = s2 as Element of REAL (N + 1) by EUCLID:22;

A84: 1 ^2 = (|.(s1 | N).| ^2) + ((s1 . (N + 1)) ^2) by REAL_NS1:10, A79;

A85: H . x2 = <:F:> . x2 by A70, FUNCT_1:47, A80;

assume A86: H . x1 = H . x2 ; :: thesis: x1 = x2

H . x1 = <:F:> . x1 by A76, A70, FUNCT_1:47;

then A87: s1 | N = <:F:> . s2 by A85, A86, A8, A77, A81

.= s2 | N by A8 ;

then 1 ^2 = (|.(s1 | N).| ^2) + ((s2 . (N + 1)) ^2) by REAL_NS1:10, A83;

then A88: ( s1 . (N + 1) = s2 . (N + 1) or s1 . (N + 1) = - (s2 . (N + 1)) ) by A84, SQUARE_1:40;

A89: ( s1 . (N + 1) > 0 or s1 . (N + 1) = 0 ) by A78;

A90: len s2 = N + 1 by CARD_1:def 7;

len s1 = N + 1 by CARD_1:def 7;

hence x1 = (s1 | N) ^ <*(s1 . (N + 1))*> by FINSEQ_3:55, A77

.= x2 by FINSEQ_3:55, A88, A89, A82, A90, A87, A81 ;

:: thesis: verum

set TD = Tdisk ((0. (TOP-REAL N)),1);

set M = m1 | (Tdisk ((0. (TOP-REAL N)),1));

A92: dom (m1 | (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

reconsider MM = m1 | (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL by TOPMETR:17, JORDAN5A:27;

A93: m1 | (Tdisk ((0. (TOP-REAL N)),1)) = m1 | the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by TMAP_1:def 4;

A94: for p being Point of (TOP-REAL N) st p in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) holds

MM . p = 1 - (|.p.| * |.p.|)

proof

A95:
the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1)
by N, BROUWER:3;
let x be Point of (TOP-REAL N); :: thesis: ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) )

(N NormF) . x = |.x.| by JGRAPH_4:def 1;

then NNF . x = |.x.| * |.x.| by VALUED_1:5;

then mNNF . x = - (|.x.| * |.x.|) by VALUED_1:8;

then m1 . x = 1 + (- (|.x.| * |.x.|)) by VALUED_1:2;

hence ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) ) by A93, FUNCT_1:49; :: thesis: verum

end;(N NormF) . x = |.x.| by JGRAPH_4:def 1;

then NNF . x = |.x.| * |.x.| by VALUED_1:5;

then mNNF . x = - (|.x.| * |.x.|) by VALUED_1:8;

then m1 . x = 1 + (- (|.x.| * |.x.|)) by VALUED_1:2;

hence ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) ) by A93, FUNCT_1:49; :: thesis: verum

A96: now :: thesis: for r being Real st r in rng MM holds

r >= 0

then
MM is nonnegative-yielding
by PARTFUN3:def 4;r >= 0

let r be Real; :: thesis: ( r in rng MM implies r >= 0 )

assume r in rng MM ; :: thesis: r >= 0

then consider x being object such that

A97: x in dom MM and

A98: MM . x = r by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL N) by A92, A95, A97;

|.x.| <= 1 by A97, A95, TOPREAL9:11;

then |.x.| * |.x.| <= 1 * 1 by XREAL_1:66;

then 1 - (|.x.| * |.x.|) >= 1 - (1 * 1) by XREAL_1:10;

hence r >= 0 by A94, A97, A98; :: thesis: verum

end;assume r in rng MM ; :: thesis: r >= 0

then consider x being object such that

A97: x in dom MM and

A98: MM . x = r by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL N) by A92, A95, A97;

|.x.| <= 1 by A97, A95, TOPREAL9:11;

then |.x.| * |.x.| <= 1 * 1 by XREAL_1:66;

then 1 - (|.x.| * |.x.|) >= 1 - (1 * 1) by XREAL_1:10;

hence r >= 0 by A94, A97, A98; :: thesis: verum

then reconsider SQR = |[(sqrt MM)]| as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL 1) ;

A99: dom (sqrt MM) = dom MM by PARTFUN3:def 5;

A100: rng (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

dom (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

then reconsider ID = id (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL N) by A100, FUNCT_2:2, A95, PRE_TOPC:26;

reconsider SQR = SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL ONE) ;

reconsider II = ID ^^ SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + ONE)) ;

reconsider II = II as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + 1)) ;

A101: dom II = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

A102: dom SQR = dom (sqrt MM) by Def1;

for y, x being object holds

( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

proof

then A128:
H " = II
by A91, A101, A74, FUNCT_1:32;
let y, x be object ; :: thesis: ( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

A114: x in dom H and

A115: y = H . x ; :: thesis: ( y in rng H & x = II . y )

consider p being Point of (TOP-REAL (N + 1)) such that

A116: x = p and

A117: p . (N + 1) >= 0 and

A118: |.p.| = 1 by A114, A17, A71, A72;

A119: p | N is FinSequence of REAL by RVSUM_1:145;

len p = N + 1 by CARD_1:def 7;

then len (p | N) = N by NAT_1:11, FINSEQ_1:59;

then reconsider pN = p | N as Point of (TOP-REAL N) by A119, TOPREAL7:17;

A121: p = pN ^ <*(p . (N + 1))*> by CARD_1:def 7, FINSEQ_3:55;

set p1 = 1 - (|.pN.| * |.pN.|);

set sp = sqrt (1 - (|.pN.| * |.pN.|));

set ssp = |[(sqrt (1 - (|.pN.| * |.pN.|)))]|;

A122: sqr <*(p . (N + 1))*> = <*((p . (N + 1)) ^2)*> by RVSUM_1:55;

A123: pN - (0. (TOP-REAL N)) = pN by VECTSP_1:18;

sqr p = (sqr pN) ^ (sqr <*(p . (N + 1))*>) by A121, RVSUM_1:144;

then Sum (sqr p) = (Sum (sqr pN)) + ((p . (N + 1)) ^2) by RVSUM_1:74, A122

.= (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5 ;

then A124: |.p.| ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5;

then |.p.| ^2 >= |.pN.| ^2 by XREAL_1:38;

then |.pN.| <= 1 by SQUARE_1:47, A118;

then A125: pN in rng H by A123, A73;

then MM . pN = 1 - (|.pN.| * |.pN.|) by A94;

then (sqrt MM) . pN = sqrt (1 - (|.pN.| * |.pN.|)) by A125, A92, PARTFUN3:def 5, A99;

then A126: SQR . pN = |[(sqrt (1 - (|.pN.| * |.pN.|)))]| by Def1, A99, A102, A125, A92;

A127: <:F:> . p = p | N by A8;

hence y in rng H by A125, A115, A116, A114, A70, FUNCT_1:47; :: thesis: x = II . y

ID . pN = pN by A125, FUNCT_1:17;

then II . pN = pN ^ |[(sqrt (1 - (|.pN.| * |.pN.|)))]| by A125, A101, A126, PRE_POLY:def 4;

then II . pN = p by A118, A124, A117, SQUARE_1:def 2, A121;

hence x = II . y by A115, A116, A127, A114, A70, FUNCT_1:47; :: thesis: verum

end;hereby :: thesis: ( x in dom H & y = H . x implies ( y in rng H & x = II . y ) )

assume that assume that

A103: y in rng H and

A104: x = II . y ; :: thesis: ( x in dom H & H . x = y )

reconsider p = y as Point of (TOP-REAL N) by A103, A73;

set p1 = 1 - (|.p.| * |.p.|);

set sp = sqrt (1 - (|.p.| * |.p.|));

set ssp = |[(sqrt (1 - (|.p.| * |.p.|)))]|;

A105: ID . p = p by A103, FUNCT_1:17;

A106: MM . p = 1 - (|.p.| * |.p.|) by A103, A94;

then (sqrt MM) . p = sqrt (1 - (|.p.| * |.p.|)) by A103, A92, PARTFUN3:def 5, A99;

then SQR . p = |[(sqrt (1 - (|.p.| * |.p.|)))]| by Def1, A99, A102, A103, A92;

then A107: II . p = p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]| by A103, A101, A105, PRE_POLY:def 4;

II . p in rng II by A103, A101, FUNCT_1:def 3;

then reconsider IIp = II . p as Point of (TOP-REAL (N + 1)) ;

MM . p in rng MM by A103, A92, FUNCT_1:def 3;

then A109: MM . p >= 0 by A96;

A110: sqr |[(sqrt (1 - (|.p.| * |.p.|)))]| = <*((sqrt (1 - (|.p.| * |.p.|))) ^2)*> by RVSUM_1:55

.= <*(MM . p)*> by A109, SQUARE_1:def 2, A106 ;

sqr IIp = (sqr p) ^ (sqr |[(sqrt (1 - (|.p.| * |.p.|)))]|) by RVSUM_1:144, A107;

then Sum (sqr IIp) = (Sum (sqr p)) + (MM . p) by A110, RVSUM_1:74

.= (|.p.| ^2) + (MM . p) by TOPREAL9:5

.= 1 by A106 ;

then A111: |.IIp.| = 1 by SQUARE_1:18;

A112: len p = N by CARD_1:def 7;

then IIp . (N + 1) = sqrt (1 - (|.p.| * |.p.|)) by A107, FINSEQ_1:42;

then A113: IIp in Sp by A106, A109, A17, A111;

hence x in dom H by A104, A71, PRE_TOPC:def 5; :: thesis: H . x = y

<:F:> . IIp = H . IIp by A113, A71, A72, A70, FUNCT_1:47;

hence H . x = (p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]|) | N by A8, A107, A104

.= (p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]|) | (dom p) by A112, FINSEQ_1:def 3

.= y by FINSEQ_1:21 ;

:: thesis: verum

end;A103: y in rng H and

A104: x = II . y ; :: thesis: ( x in dom H & H . x = y )

reconsider p = y as Point of (TOP-REAL N) by A103, A73;

set p1 = 1 - (|.p.| * |.p.|);

set sp = sqrt (1 - (|.p.| * |.p.|));

set ssp = |[(sqrt (1 - (|.p.| * |.p.|)))]|;

A105: ID . p = p by A103, FUNCT_1:17;

A106: MM . p = 1 - (|.p.| * |.p.|) by A103, A94;

then (sqrt MM) . p = sqrt (1 - (|.p.| * |.p.|)) by A103, A92, PARTFUN3:def 5, A99;

then SQR . p = |[(sqrt (1 - (|.p.| * |.p.|)))]| by Def1, A99, A102, A103, A92;

then A107: II . p = p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]| by A103, A101, A105, PRE_POLY:def 4;

II . p in rng II by A103, A101, FUNCT_1:def 3;

then reconsider IIp = II . p as Point of (TOP-REAL (N + 1)) ;

MM . p in rng MM by A103, A92, FUNCT_1:def 3;

then A109: MM . p >= 0 by A96;

A110: sqr |[(sqrt (1 - (|.p.| * |.p.|)))]| = <*((sqrt (1 - (|.p.| * |.p.|))) ^2)*> by RVSUM_1:55

.= <*(MM . p)*> by A109, SQUARE_1:def 2, A106 ;

sqr IIp = (sqr p) ^ (sqr |[(sqrt (1 - (|.p.| * |.p.|)))]|) by RVSUM_1:144, A107;

then Sum (sqr IIp) = (Sum (sqr p)) + (MM . p) by A110, RVSUM_1:74

.= (|.p.| ^2) + (MM . p) by TOPREAL9:5

.= 1 by A106 ;

then A111: |.IIp.| = 1 by SQUARE_1:18;

A112: len p = N by CARD_1:def 7;

then IIp . (N + 1) = sqrt (1 - (|.p.| * |.p.|)) by A107, FINSEQ_1:42;

then A113: IIp in Sp by A106, A109, A17, A111;

hence x in dom H by A104, A71, PRE_TOPC:def 5; :: thesis: H . x = y

<:F:> . IIp = H . IIp by A113, A71, A72, A70, FUNCT_1:47;

hence H . x = (p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]|) | N by A8, A107, A104

.= (p ^ |[(sqrt (1 - (|.p.| * |.p.|)))]|) | (dom p) by A112, FINSEQ_1:def 3

.= y by FINSEQ_1:21 ;

:: thesis: verum

A114: x in dom H and

A115: y = H . x ; :: thesis: ( y in rng H & x = II . y )

consider p being Point of (TOP-REAL (N + 1)) such that

A116: x = p and

A117: p . (N + 1) >= 0 and

A118: |.p.| = 1 by A114, A17, A71, A72;

A119: p | N is FinSequence of REAL by RVSUM_1:145;

len p = N + 1 by CARD_1:def 7;

then len (p | N) = N by NAT_1:11, FINSEQ_1:59;

then reconsider pN = p | N as Point of (TOP-REAL N) by A119, TOPREAL7:17;

A121: p = pN ^ <*(p . (N + 1))*> by CARD_1:def 7, FINSEQ_3:55;

set p1 = 1 - (|.pN.| * |.pN.|);

set sp = sqrt (1 - (|.pN.| * |.pN.|));

set ssp = |[(sqrt (1 - (|.pN.| * |.pN.|)))]|;

A122: sqr <*(p . (N + 1))*> = <*((p . (N + 1)) ^2)*> by RVSUM_1:55;

A123: pN - (0. (TOP-REAL N)) = pN by VECTSP_1:18;

sqr p = (sqr pN) ^ (sqr <*(p . (N + 1))*>) by A121, RVSUM_1:144;

then Sum (sqr p) = (Sum (sqr pN)) + ((p . (N + 1)) ^2) by RVSUM_1:74, A122

.= (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5 ;

then A124: |.p.| ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5;

then |.p.| ^2 >= |.pN.| ^2 by XREAL_1:38;

then |.pN.| <= 1 by SQUARE_1:47, A118;

then A125: pN in rng H by A123, A73;

then MM . pN = 1 - (|.pN.| * |.pN.|) by A94;

then (sqrt MM) . pN = sqrt (1 - (|.pN.| * |.pN.|)) by A125, A92, PARTFUN3:def 5, A99;

then A126: SQR . pN = |[(sqrt (1 - (|.pN.| * |.pN.|)))]| by Def1, A99, A102, A125, A92;

A127: <:F:> . p = p | N by A8;

hence y in rng H by A125, A115, A116, A114, A70, FUNCT_1:47; :: thesis: x = II . y

ID . pN = pN by A125, FUNCT_1:17;

then II . pN = pN ^ |[(sqrt (1 - (|.pN.| * |.pN.|)))]| by A125, A101, A126, PRE_POLY:def 4;

then II . pN = p by A118, A124, A117, SQUARE_1:def 2, A121;

hence x = II . y by A115, A116, A127, A114, A70, FUNCT_1:47; :: thesis: verum

dom (0* (N + 1)) = Seg (N + 1) ;

then N0 . (N + 1) = 1 by A68, FUNCT_7:31;

then A129: N0 in Sp by A69, A17;

for P being Subset of ((TOP-REAL (N + 1)) | Sp) holds

( P is open iff H .: P is open )

proof

hence
H is being_homeomorphism
by A71, A74, A91, A129, TOPGRP_1:25; :: thesis: verum
let P be Subset of ((TOP-REAL (N + 1)) | Sp); :: thesis: ( P is open iff H .: P is open )

for i being Nat st i in dom F holds

for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

<:F:> | ((TOP-REAL (N + 1)) | Sp) = <:F:> | Sp by TMAP_1:def 4, A72;

then A135: H is continuous by A134, A129, A70, PRE_TOPC:27;

H " (H .: P) = P by A71, A75, FUNCT_1:def 4, FUNCT_1:94;

hence P is open by A138, TOPS_2:43, A135, A67; :: thesis: verum

end;for i being Nat st i in dom F holds

for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

proof

then A134:
<:F:> is continuous
by TIETZE_2:21;
let i be Nat; :: thesis: ( i in dom F implies for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous )

assume A130: i in dom F ; :: thesis: for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

i <= N by A130, A6, FINSEQ_1:1;

then A131: i <= N + 1 by NAT_1:13;

let h be Function of (TOP-REAL (N + 1)),R^1; :: thesis: ( h = F . i implies h is continuous )

assume A132: h = F . i ; :: thesis: h is continuous

A133: h = PROJ ((N + 1),i) by A130, A132, A7;

1 <= i by A130, A6, FINSEQ_1:1;

then i in Seg (N + 1) by A131;

hence h is continuous by A133, TOPREALC:57; :: thesis: verum

end;h is continuous )

assume A130: i in dom F ; :: thesis: for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

i <= N by A130, A6, FINSEQ_1:1;

then A131: i <= N + 1 by NAT_1:13;

let h be Function of (TOP-REAL (N + 1)),R^1; :: thesis: ( h = F . i implies h is continuous )

assume A132: h = F . i ; :: thesis: h is continuous

A133: h = PROJ ((N + 1),i) by A130, A132, A7;

1 <= i by A130, A6, FINSEQ_1:1;

then i in Seg (N + 1) by A131;

hence h is continuous by A133, TOPREALC:57; :: thesis: verum

<:F:> | ((TOP-REAL (N + 1)) | Sp) = <:F:> | Sp by TMAP_1:def 4, A72;

then A135: H is continuous by A134, A129, A70, PRE_TOPC:27;

hereby :: thesis: ( H .: P is open implies P is open )

assume A138:
H .: P is open
; :: thesis: P is open
rng II = dom H
by A128, A91, FUNCT_1:33;

then reconsider ii = II as Function of (Tdisk ((0. (TOP-REAL N)),1)),((TOP-REAL (N + 1)) | Sp) by FUNCT_2:2, A101;

assume A136: P is open ; :: thesis: H .: P is open

A137: ii is continuous by PRE_TOPC:27;

not dom H is empty by A73, A71;

then ii " P is open by A137, A71, A136, TOPS_2:43;

hence H .: P is open by A75, FUNCT_1:def 4, FUNCT_1:84, A128; :: thesis: verum

end;then reconsider ii = II as Function of (Tdisk ((0. (TOP-REAL N)),1)),((TOP-REAL (N + 1)) | Sp) by FUNCT_2:2, A101;

assume A136: P is open ; :: thesis: H .: P is open

A137: ii is continuous by PRE_TOPC:27;

not dom H is empty by A73, A71;

then ii " P is open by A137, A71, A136, TOPS_2:43;

hence H .: P is open by A75, FUNCT_1:def 4, FUNCT_1:84, A128; :: thesis: verum

H " (H .: P) = P by A71, A75, FUNCT_1:def 4, FUNCT_1:94;

hence P is open by A138, TOPS_2:43, A135, A67; :: thesis: verum

assume A139: H = <:F:> | Sn ; :: thesis: H is being_homeomorphism

A140: dom H = [#] ((TOP-REAL (N + 1)) | Sn) by FUNCT_2:def 1;

A141: [#] ((TOP-REAL (N + 1)) | Sn) = Sn by PRE_TOPC:def 5;

then A142: rng H = (<:F:> | Sn) .: Sn by A140, A139, RELAT_1:113

.= cl_Ball ((0. (TOP-REAL N)),1) by A29, A54, RELAT_1:129 ;

then A143: rng H = [#] (Tdisk ((0. (TOP-REAL N)),1)) by PRE_TOPC:def 5;

A144: for x1, x2 being object st x1 in dom H & x2 in dom H & H . x1 = H . x2 holds

x1 = x2

proof

then A160:
H is one-to-one
;
let x1, x2 be object ; :: thesis: ( x1 in dom H & x2 in dom H & H . x1 = H . x2 implies x1 = x2 )

assume A145: x1 in dom H ; :: thesis: ( not x2 in dom H or not H . x1 = H . x2 or x1 = x2 )

then consider s1 being Point of (TOP-REAL (N + 1)) such that

A146: x1 = s1 and

A147: s1 . (N + 1) <= 0 and

A148: |.s1.| = 1 by A28, A140, A141;

assume A149: x2 in dom H ; :: thesis: ( not H . x1 = H . x2 or x1 = x2 )

then consider s2 being Point of (TOP-REAL (N + 1)) such that

A150: x2 = s2 and

A151: s2 . (N + 1) <= 0 and

A152: |.s2.| = 1 by A28, A140, A141;

reconsider s1 = s1, s2 = s2 as Element of REAL (N + 1) by EUCLID:22;

A153: 1 ^2 = (|.(s1 | N).| ^2) + ((s1 . (N + 1)) ^2) by REAL_NS1:10, A148;

A154: H . x2 = <:F:> . x2 by A139, FUNCT_1:47, A149;

assume A155: H . x1 = H . x2 ; :: thesis: x1 = x2

H . x1 = <:F:> . x1 by A145, A139, FUNCT_1:47;

then A156: s1 | N = <:F:> . s2 by A154, A155, A8, A146, A150

.= s2 | N by A8 ;

then 1 ^2 = (|.(s1 | N).| ^2) + ((s2 . (N + 1)) ^2) by REAL_NS1:10, A152;

then A157: ( s1 . (N + 1) = s2 . (N + 1) or s1 . (N + 1) = - (s2 . (N + 1)) ) by A153, SQUARE_1:40;

A158: ( s1 . (N + 1) < 0 or s1 . (N + 1) = 0 ) by A147;

A159: len s2 = N + 1 by CARD_1:def 7;

len s1 = N + 1 by CARD_1:def 7;

hence x1 = (s1 | N) ^ <*(s1 . (N + 1))*> by FINSEQ_3:55, A146

.= x2 by FINSEQ_3:55, A157, A158, A151, A159, A156, A150 ;

:: thesis: verum

end;assume A145: x1 in dom H ; :: thesis: ( not x2 in dom H or not H . x1 = H . x2 or x1 = x2 )

then consider s1 being Point of (TOP-REAL (N + 1)) such that

A146: x1 = s1 and

A147: s1 . (N + 1) <= 0 and

A148: |.s1.| = 1 by A28, A140, A141;

assume A149: x2 in dom H ; :: thesis: ( not H . x1 = H . x2 or x1 = x2 )

then consider s2 being Point of (TOP-REAL (N + 1)) such that

A150: x2 = s2 and

A151: s2 . (N + 1) <= 0 and

A152: |.s2.| = 1 by A28, A140, A141;

reconsider s1 = s1, s2 = s2 as Element of REAL (N + 1) by EUCLID:22;

A153: 1 ^2 = (|.(s1 | N).| ^2) + ((s1 . (N + 1)) ^2) by REAL_NS1:10, A148;

A154: H . x2 = <:F:> . x2 by A139, FUNCT_1:47, A149;

assume A155: H . x1 = H . x2 ; :: thesis: x1 = x2

H . x1 = <:F:> . x1 by A145, A139, FUNCT_1:47;

then A156: s1 | N = <:F:> . s2 by A154, A155, A8, A146, A150

.= s2 | N by A8 ;

then 1 ^2 = (|.(s1 | N).| ^2) + ((s2 . (N + 1)) ^2) by REAL_NS1:10, A152;

then A157: ( s1 . (N + 1) = s2 . (N + 1) or s1 . (N + 1) = - (s2 . (N + 1)) ) by A153, SQUARE_1:40;

A158: ( s1 . (N + 1) < 0 or s1 . (N + 1) = 0 ) by A147;

A159: len s2 = N + 1 by CARD_1:def 7;

len s1 = N + 1 by CARD_1:def 7;

hence x1 = (s1 | N) ^ <*(s1 . (N + 1))*> by FINSEQ_3:55, A146

.= x2 by FINSEQ_3:55, A157, A158, A151, A159, A156, A150 ;

:: thesis: verum

set TD = Tdisk ((0. (TOP-REAL N)),1);

set M = m1 | (Tdisk ((0. (TOP-REAL N)),1));

A161: dom (m1 | (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

reconsider MM = m1 | (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL by TOPMETR:17, JORDAN5A:27;

reconsider Msqr = - (sqrt MM) as Function of (Tdisk ((0. (TOP-REAL N)),1)),REAL ;

A162: m1 | (Tdisk ((0. (TOP-REAL N)),1)) = m1 | the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by TMAP_1:def 4;

A163: for p being Point of (TOP-REAL N) st p in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) holds

MM . p = 1 - (|.p.| * |.p.|)

proof

A164:
the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1)
by N, BROUWER:3;
let x be Point of (TOP-REAL N); :: thesis: ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) )

(N NormF) . x = |.x.| by JGRAPH_4:def 1;

then NNF . x = |.x.| * |.x.| by VALUED_1:5;

then mNNF . x = - (|.x.| * |.x.|) by VALUED_1:8;

then m1 . x = 1 + (- (|.x.| * |.x.|)) by VALUED_1:2;

hence ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) ) by A162, FUNCT_1:49; :: thesis: verum

end;(N NormF) . x = |.x.| by JGRAPH_4:def 1;

then NNF . x = |.x.| * |.x.| by VALUED_1:5;

then mNNF . x = - (|.x.| * |.x.|) by VALUED_1:8;

then m1 . x = 1 + (- (|.x.| * |.x.|)) by VALUED_1:2;

hence ( x in the carrier of (Tdisk ((0. (TOP-REAL N)),1)) implies MM . x = 1 - (|.x.| * |.x.|) ) by A162, FUNCT_1:49; :: thesis: verum

A165: now :: thesis: for r being Real st r in rng MM holds

r >= 0

then
MM is nonnegative-yielding
by PARTFUN3:def 4;r >= 0

let r be Real; :: thesis: ( r in rng MM implies r >= 0 )

assume r in rng MM ; :: thesis: r >= 0

then consider x being object such that

A166: x in dom MM and

A167: MM . x = r by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL N) by A161, A164, A166;

|.x.| <= 1 by A166, A164, TOPREAL9:11;

then |.x.| * |.x.| <= 1 * 1 by XREAL_1:66;

then 1 - (|.x.| * |.x.|) >= 1 - (1 * 1) by XREAL_1:10;

hence r >= 0 by A163, A166, A167; :: thesis: verum

end;assume r in rng MM ; :: thesis: r >= 0

then consider x being object such that

A166: x in dom MM and

A167: MM . x = r by FUNCT_1:def 3;

reconsider x = x as Point of (TOP-REAL N) by A161, A164, A166;

|.x.| <= 1 by A166, A164, TOPREAL9:11;

then |.x.| * |.x.| <= 1 * 1 by XREAL_1:66;

then 1 - (|.x.| * |.x.|) >= 1 - (1 * 1) by XREAL_1:10;

hence r >= 0 by A163, A166, A167; :: thesis: verum

then reconsider SQR = |[Msqr]| as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL 1) ;

A168: dom (sqrt MM) = dom MM by PARTFUN3:def 5;

A169: rng (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

dom (id (Tdisk ((0. (TOP-REAL N)),1))) = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) ;

then reconsider ID = id (Tdisk ((0. (TOP-REAL N)),1)) as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL N) by A169, FUNCT_2:2, A164, PRE_TOPC:26;

reconsider SQR = SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL ONE) ;

reconsider II = ID ^^ SQR as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + ONE)) ;

reconsider II = II as continuous Function of (Tdisk ((0. (TOP-REAL N)),1)),(TOP-REAL (N + 1)) ;

A170: dom II = the carrier of (Tdisk ((0. (TOP-REAL N)),1)) by FUNCT_2:def 1;

dom (- (sqrt MM)) = dom (sqrt MM) by VALUED_1:8;

then A171: dom SQR = dom (sqrt MM) by Def1;

for y, x being object holds

( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

proof

then A198:
H " = II
by A160, A170, A143, FUNCT_1:32;
let y, x be object ; :: thesis: ( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )

A183: x in dom H and

A184: y = H . x ; :: thesis: ( y in rng H & x = II . y )

consider p being Point of (TOP-REAL (N + 1)) such that

A185: x = p and

A186: p . (N + 1) <= 0 and

A187: |.p.| = 1 by A183, A28, A140, A141;

A188: p | N is FinSequence of REAL by RVSUM_1:145;

len p = N + 1 by CARD_1:def 7;

then len (p | N) = N by NAT_1:11, FINSEQ_1:59;

then reconsider pN = p | N as Point of (TOP-REAL N) by A188, TOPREAL7:17;

A190: p = pN ^ <*(p . (N + 1))*> by CARD_1:def 7, FINSEQ_3:55;

A191: sqr <*(p . (N + 1))*> = <*((p . (N + 1)) ^2)*> by RVSUM_1:55;

sqr p = (sqr pN) ^ (sqr <*(p . (N + 1))*>) by A190, RVSUM_1:144;

then A192: Sum (sqr p) = (Sum (sqr pN)) + ((p . (N + 1)) ^2) by RVSUM_1:74, A191

.= (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5 ;

then |.p.| ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5;

then |.p.| ^2 >= |.pN.| ^2 by XREAL_1:38;

then A193: |.pN.| <= 1 by SQUARE_1:47, A187;

set p1 = 1 - (|.pN.| * |.pN.|);

set sp = sqrt (1 - (|.pN.| * |.pN.|));

set ssp = |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]|;

pN - (0. (TOP-REAL N)) = pN by VECTSP_1:18;

then A194: pN in rng H by A193, A142;

then MM . pN = 1 - (|.pN.| * |.pN.|) by A163;

then (sqrt MM) . pN = sqrt (1 - (|.pN.| * |.pN.|)) by A194, A161, PARTFUN3:def 5, A168;

then Msqr . pN = - (sqrt (1 - (|.pN.| * |.pN.|))) by VALUED_1:8;

then A195: SQR . pN = |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]| by Def1, A168, A171, A194, A161;

1 ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by A187, A192, TOPREAL9:5;

then A196: - (p . (N + 1)) = sqrt (1 - (|.pN.| ^2)) by A186, SQUARE_1:23;

A197: <:F:> . p = p | N by A8;

hence y in rng H by A194, A184, A185, A183, A139, FUNCT_1:47; :: thesis: x = II . y

ID . pN = pN by A194, FUNCT_1:17;

then II . pN = pN ^ |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]| by A194, A170, A195, PRE_POLY:def 4;

hence x = II . y by A196, A190, A184, A185, A197, A183, A139, FUNCT_1:47; :: thesis: verum

end;hereby :: thesis: ( x in dom H & y = H . x implies ( y in rng H & x = II . y ) )

assume that assume that

A172: y in rng H and

A173: x = II . y ; :: thesis: ( x in dom H & H . x = y )

reconsider p = y as Point of (TOP-REAL N) by A172, A142;

set p1 = 1 - (|.p.| * |.p.|);

set sp = sqrt (1 - (|.p.| * |.p.|));

set ssp = |[(- (sqrt (1 - (|.p.| * |.p.|))))]|;

A174: ID . p = p by A172, FUNCT_1:17;

A175: MM . p = 1 - (|.p.| * |.p.|) by A172, A163;

then (sqrt MM) . p = sqrt (1 - (|.p.| * |.p.|)) by A172, A161, PARTFUN3:def 5, A168;

then Msqr . p = - (sqrt (1 - (|.p.| * |.p.|))) by VALUED_1:8;

then SQR . p = |[(- (sqrt (1 - (|.p.| * |.p.|))))]| by Def1, A168, A171, A172, A161;

then A176: II . p = p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]| by A172, A170, A174, PRE_POLY:def 4;

II . p in rng II by A172, A170, FUNCT_1:def 3;

then reconsider IIp = II . p as Point of (TOP-REAL (N + 1)) ;

MM . p in rng MM by A172, A161, FUNCT_1:def 3;

then A178: MM . p >= 0 by A165;

A179: sqr IIp = (sqr p) ^ (sqr |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) by RVSUM_1:144, A176;

(sqrt (1 - (|.p.| * |.p.|))) ^2 = (- (sqrt (1 - (|.p.| * |.p.|)))) ^2 ;

then sqr |[(- (sqrt (1 - (|.p.| * |.p.|))))]| = <*((sqrt (1 - (|.p.| * |.p.|))) ^2)*> by RVSUM_1:55

.= <*(MM . p)*> by A178, SQUARE_1:def 2, A175 ;

then Sum (sqr IIp) = (Sum (sqr p)) + (MM . p) by A179, RVSUM_1:74

.= (|.p.| ^2) + (MM . p) by TOPREAL9:5

.= 1 by A175 ;

then A180: |.IIp.| = 1 by SQUARE_1:18;

A181: len p = N by CARD_1:def 7;

then IIp . (N + 1) = - (sqrt (1 - (|.p.| * |.p.|))) by A176, FINSEQ_1:42;

then A182: IIp in Sn by A175, A178, A28, A180;

hence x in dom H by A173, A140, PRE_TOPC:def 5; :: thesis: H . x = y

<:F:> . IIp = H . IIp by A182, A140, A141, A139, FUNCT_1:47;

hence H . x = (p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) | N by A8, A176, A173

.= (p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) | (dom p) by A181, FINSEQ_1:def 3

.= y by FINSEQ_1:21 ;

:: thesis: verum

end;A172: y in rng H and

A173: x = II . y ; :: thesis: ( x in dom H & H . x = y )

reconsider p = y as Point of (TOP-REAL N) by A172, A142;

set p1 = 1 - (|.p.| * |.p.|);

set sp = sqrt (1 - (|.p.| * |.p.|));

set ssp = |[(- (sqrt (1 - (|.p.| * |.p.|))))]|;

A174: ID . p = p by A172, FUNCT_1:17;

A175: MM . p = 1 - (|.p.| * |.p.|) by A172, A163;

then (sqrt MM) . p = sqrt (1 - (|.p.| * |.p.|)) by A172, A161, PARTFUN3:def 5, A168;

then Msqr . p = - (sqrt (1 - (|.p.| * |.p.|))) by VALUED_1:8;

then SQR . p = |[(- (sqrt (1 - (|.p.| * |.p.|))))]| by Def1, A168, A171, A172, A161;

then A176: II . p = p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]| by A172, A170, A174, PRE_POLY:def 4;

II . p in rng II by A172, A170, FUNCT_1:def 3;

then reconsider IIp = II . p as Point of (TOP-REAL (N + 1)) ;

MM . p in rng MM by A172, A161, FUNCT_1:def 3;

then A178: MM . p >= 0 by A165;

A179: sqr IIp = (sqr p) ^ (sqr |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) by RVSUM_1:144, A176;

(sqrt (1 - (|.p.| * |.p.|))) ^2 = (- (sqrt (1 - (|.p.| * |.p.|)))) ^2 ;

then sqr |[(- (sqrt (1 - (|.p.| * |.p.|))))]| = <*((sqrt (1 - (|.p.| * |.p.|))) ^2)*> by RVSUM_1:55

.= <*(MM . p)*> by A178, SQUARE_1:def 2, A175 ;

then Sum (sqr IIp) = (Sum (sqr p)) + (MM . p) by A179, RVSUM_1:74

.= (|.p.| ^2) + (MM . p) by TOPREAL9:5

.= 1 by A175 ;

then A180: |.IIp.| = 1 by SQUARE_1:18;

A181: len p = N by CARD_1:def 7;

then IIp . (N + 1) = - (sqrt (1 - (|.p.| * |.p.|))) by A176, FINSEQ_1:42;

then A182: IIp in Sn by A175, A178, A28, A180;

hence x in dom H by A173, A140, PRE_TOPC:def 5; :: thesis: H . x = y

<:F:> . IIp = H . IIp by A182, A140, A141, A139, FUNCT_1:47;

hence H . x = (p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) | N by A8, A176, A173

.= (p ^ |[(- (sqrt (1 - (|.p.| * |.p.|))))]|) | (dom p) by A181, FINSEQ_1:def 3

.= y by FINSEQ_1:21 ;

:: thesis: verum

A183: x in dom H and

A184: y = H . x ; :: thesis: ( y in rng H & x = II . y )

consider p being Point of (TOP-REAL (N + 1)) such that

A185: x = p and

A186: p . (N + 1) <= 0 and

A187: |.p.| = 1 by A183, A28, A140, A141;

A188: p | N is FinSequence of REAL by RVSUM_1:145;

len p = N + 1 by CARD_1:def 7;

then len (p | N) = N by NAT_1:11, FINSEQ_1:59;

then reconsider pN = p | N as Point of (TOP-REAL N) by A188, TOPREAL7:17;

A190: p = pN ^ <*(p . (N + 1))*> by CARD_1:def 7, FINSEQ_3:55;

A191: sqr <*(p . (N + 1))*> = <*((p . (N + 1)) ^2)*> by RVSUM_1:55;

sqr p = (sqr pN) ^ (sqr <*(p . (N + 1))*>) by A190, RVSUM_1:144;

then A192: Sum (sqr p) = (Sum (sqr pN)) + ((p . (N + 1)) ^2) by RVSUM_1:74, A191

.= (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5 ;

then |.p.| ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by TOPREAL9:5;

then |.p.| ^2 >= |.pN.| ^2 by XREAL_1:38;

then A193: |.pN.| <= 1 by SQUARE_1:47, A187;

set p1 = 1 - (|.pN.| * |.pN.|);

set sp = sqrt (1 - (|.pN.| * |.pN.|));

set ssp = |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]|;

pN - (0. (TOP-REAL N)) = pN by VECTSP_1:18;

then A194: pN in rng H by A193, A142;

then MM . pN = 1 - (|.pN.| * |.pN.|) by A163;

then (sqrt MM) . pN = sqrt (1 - (|.pN.| * |.pN.|)) by A194, A161, PARTFUN3:def 5, A168;

then Msqr . pN = - (sqrt (1 - (|.pN.| * |.pN.|))) by VALUED_1:8;

then A195: SQR . pN = |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]| by Def1, A168, A171, A194, A161;

1 ^2 = (|.pN.| ^2) + ((p . (N + 1)) ^2) by A187, A192, TOPREAL9:5;

then A196: - (p . (N + 1)) = sqrt (1 - (|.pN.| ^2)) by A186, SQUARE_1:23;

A197: <:F:> . p = p | N by A8;

hence y in rng H by A194, A184, A185, A183, A139, FUNCT_1:47; :: thesis: x = II . y

ID . pN = pN by A194, FUNCT_1:17;

then II . pN = pN ^ |[(- (sqrt (1 - (|.pN.| * |.pN.|))))]| by A194, A170, A195, PRE_POLY:def 4;

hence x = II . y by A196, A190, A184, A185, A197, A183, A139, FUNCT_1:47; :: thesis: verum

|.N0.| = |.(- 1).| by TOPREALC:13, A3

.= - (- 1) by ABSVALUE:def 1 ;

then A199: N0 in Sn by A28, A4;

for P being Subset of ((TOP-REAL (N + 1)) | Sn) holds

( P is open iff H .: P is open )

proof

hence
H is being_homeomorphism
by A140, A143, A160, A199, TOPGRP_1:25; :: thesis: verum
let P be Subset of ((TOP-REAL (N + 1)) | Sn); :: thesis: ( P is open iff H .: P is open )

for i being Nat st i in dom F holds

for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

<:F:> | ((TOP-REAL (N + 1)) | Sn) = <:F:> | Sn by TMAP_1:def 4, A141;

then A205: H is continuous by A204, A199, A139, PRE_TOPC:27;

H " (H .: P) = P by A140, A144, FUNCT_1:def 4, FUNCT_1:94;

hence P is open by A208, TOPS_2:43, A205, A2; :: thesis: verum

end;for i being Nat st i in dom F holds

for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

proof

then A204:
<:F:> is continuous
by TIETZE_2:21;
let i be Nat; :: thesis: ( i in dom F implies for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous )

assume A200: i in dom F ; :: thesis: for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

i <= N by A200, A6, FINSEQ_1:1;

then A201: i <= N + 1 by NAT_1:13;

let h be Function of (TOP-REAL (N + 1)),R^1; :: thesis: ( h = F . i implies h is continuous )

assume A202: h = F . i ; :: thesis: h is continuous

A203: h = PROJ ((N + 1),i) by A200, A202, A7;

1 <= i by A200, A6, FINSEQ_1:1;

then i in Seg (N + 1) by A201;

hence h is continuous by A203, TOPREALC:57; :: thesis: verum

end;h is continuous )

assume A200: i in dom F ; :: thesis: for h being Function of (TOP-REAL (N + 1)),R^1 st h = F . i holds

h is continuous

i <= N by A200, A6, FINSEQ_1:1;

then A201: i <= N + 1 by NAT_1:13;

let h be Function of (TOP-REAL (N + 1)),R^1; :: thesis: ( h = F . i implies h is continuous )

assume A202: h = F . i ; :: thesis: h is continuous

A203: h = PROJ ((N + 1),i) by A200, A202, A7;

1 <= i by A200, A6, FINSEQ_1:1;

then i in Seg (N + 1) by A201;

hence h is continuous by A203, TOPREALC:57; :: thesis: verum

<:F:> | ((TOP-REAL (N + 1)) | Sn) = <:F:> | Sn by TMAP_1:def 4, A141;

then A205: H is continuous by A204, A199, A139, PRE_TOPC:27;

hereby :: thesis: ( H .: P is open implies P is open )

assume A208:
H .: P is open
; :: thesis: P is open
rng II = dom H
by A198, A160, FUNCT_1:33;

then reconsider ii = II as Function of (Tdisk ((0. (TOP-REAL N)),1)),((TOP-REAL (N + 1)) | Sn) by FUNCT_2:2, A170;

assume A206: P is open ; :: thesis: H .: P is open

A207: ii is continuous by PRE_TOPC:27;

not dom H is empty by A142, A140;

then ii " P is open by A207, A140, A206, TOPS_2:43;

hence H .: P is open by A144, FUNCT_1:def 4, FUNCT_1:84, A198; :: thesis: verum

end;then reconsider ii = II as Function of (Tdisk ((0. (TOP-REAL N)),1)),((TOP-REAL (N + 1)) | Sn) by FUNCT_2:2, A170;

assume A206: P is open ; :: thesis: H .: P is open

A207: ii is continuous by PRE_TOPC:27;

not dom H is empty by A142, A140;

then ii " P is open by A207, A140, A206, TOPS_2:43;

hence H .: P is open by A144, FUNCT_1:def 4, FUNCT_1:84, A198; :: thesis: verum

H " (H .: P) = P by A140, A144, FUNCT_1:def 4, FUNCT_1:94;

hence P is open by A208, TOPS_2:43, A205, A2; :: thesis: verum