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 ) )
proof
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;
now :: thesis: for i being Nat st 1 <= i & i <= N holds
Fs . 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;
hence <:F:> . s = s | N by A9, A10, FINSEQ_1:59, A5; :: thesis: verum
end;
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
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
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 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
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
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;
A38: Sphere ((0. (TOP-REAL N)),1) c= <:F:> .: (Sn /\ Sp)
proof
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;
A48: <:F:> .: Sp c= cl_Ball ((0. (TOP-REAL N)),1)
proof
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;
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
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
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;
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
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
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;
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
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
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
proof
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;
then A91: H is one-to-one ;
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
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;
A95: the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by N, BROUWER:3;
A96: now :: thesis: for r being Real st r in rng MM holds
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;
then MM is nonnegative-yielding by PARTFUN3:def 4;
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
let y, x be object ; :: thesis: ( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )
hereby :: thesis: ( x in dom H & y = H . x implies ( y in rng H & x = II . y ) )
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;
assume that
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;
then A128: H " = II by A91, A101, A74, FUNCT_1:32;
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
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
proof
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;
then A134: <:F:> is continuous by TIETZE_2:21;
<: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 )
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;
assume A138: H .: P is open ; :: thesis: P is open
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;
hence H is being_homeomorphism by A71, A74, A91, A129, TOPGRP_1:25; :: thesis: verum
end;
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 )
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
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;
then A160: H is one-to-one ;
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
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;
A164: the carrier of (Tdisk ((0. (TOP-REAL N)),1)) = cl_Ball ((0. (TOP-REAL N)),1) by N, BROUWER:3;
A165: now :: thesis: for r being Real st r in rng MM holds
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;
then MM is nonnegative-yielding by PARTFUN3:def 4;
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
let y, x be object ; :: thesis: ( y in rng H & x = II . y iff ( x in dom H & y = H . x ) )
hereby :: thesis: ( x in dom H & y = H . x implies ( y in rng H & x = II . y ) )
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;
assume that
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;
then A198: H " = II by A160, A170, A143, FUNCT_1:32;
|.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
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
proof
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;
then A204: <:F:> is continuous by TIETZE_2:21;
<: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 )
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;
assume A208: H .: P is open ; :: thesis: P is open
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;
hence H is being_homeomorphism by A140, A143, A160, A199, TOPGRP_1:25; :: thesis: verum