let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real st r > 0 holds
ind (Sphere (p,r)) = n - 1
let p be Point of (TOP-REAL n); :: thesis: for r being Real st r > 0 holds
ind (Sphere (p,r)) = n - 1
let r be Real; :: thesis: ( r > 0 implies ind (Sphere (p,r)) = n - 1 )
set TR = TOP-REAL n;
A1: for i being Nat
for A, B being Subset of (TOP-REAL n) st ind A <= i & ind B <= i & A is closed holds
ind (A \/ B) <= i

proof

let i be Nat; :: thesis: for A, B being Subset of (TOP-REAL n) st ind A <= i & ind B <= i & A is closed holds
ind (A \/ B) <= i
let A, B be Subset of (TOP-REAL n); :: thesis: ( ind A <= i & ind B <= i & A is closed implies ind (A \/ B) <= i )
set TT = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #);
assume that
A2: ind A <= i and
A3: ind B <= i and
A4: A is closed ; :: thesis: ind (A \/ B) <= i
reconsider a = A, b = B, AB = A \/ B as Subset of TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) ;
A5: a is closed by A4, PRE_TOPC:31;
A6: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) | AB is second-countable ;
A7: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
A8: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = (TOP-REAL n) | ([#] (TOP-REAL n)) by TSEP_1:93;
then A9: ind b <= i by TOPDIM_1:22, A3;
ind a <= i by A8, TOPDIM_1:22, A2;
then ind AB <= i by A9, A5, A8, A7, A6, TOPDIM_2:5;
hence ind (A \/ B) <= i by TOPDIM_1:22, A8; :: thesis: verum

end;

assume A10: r > 0 ; :: thesis: ind (Sphere (p,r)) = n - 1

per cases ( n = 0 or n = 1 or n > 1 ) by NAT_1:25;

suppose A11: n = 0 ; :: thesis: ind (Sphere (p,r)) = n - 1

then A12: p = 0. (TOP-REAL n) by EUCLID:77;
Sphere (p,r) = {}

proof

assume Sphere (p,r) <> {} ; :: thesis: contradiction
then consider x being object such that
A13: x in Sphere (p,r) by XBOOLE_0:def 1;
reconsider x = x as Point of (TOP-REAL n) by A13;
x = 0. (TOP-REAL n) by A11, EUCLID:77
.= 0* n by EUCLID:66 ;
then |.x.| = 0 by EUCLID:7;
hence contradiction by A12, A13, TOPREAL9:12, A10; :: thesis: verum

end;

hence ind (Sphere (p,r)) = n - 1 by TOPDIM_1:6, A11; :: thesis: verum

end;

suppose A15: n = 1 ; :: thesis: ind (Sphere (p,r)) = n - 1

then consider u being Real such that
A16: p = <*u*> by JORDAN2B:20;
set u1 = |[(u - r)]|;
set u2 = |[(u + r)]|;
card {|[(u + r)]|} = 1 by CARD_1:30;
then A17: ind {|[(u + r)]|} = 0 by TOPDIM_1:8, NAT_1:14;
card {|[(u - r)]|} = 1 by CARD_1:30;
then ind {|[(u - r)]|} = 0 by TOPDIM_1:8, NAT_1:14;
then A18: ind ({|[(u - r)]|} \/ {|[(u + r)]|}) = 0 by A17, A15, A1;
{<*(u - r)*>,<*(u + r)*>} = Fr (Ball (p,r)) by A15, TOPDIM_2:18, A16, A10
.= Sphere (p,r) by A15, A10, JORDAN:24 ;
hence ind (Sphere (p,r)) = n - 1 by A18, ENUMSET1:1, A15; :: thesis: verum

end;

suppose A19: n > 1 ; :: thesis: ind (Sphere (p,r)) = n - 1

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
reconsider n1 = n1 as non zero Element of NAT by A19;
set n2 = n1 + 1;
set Tn1 = TOP-REAL n1;
set Tn2 = TOP-REAL (n1 + 1);
set S = Sphere ((0. (TOP-REAL (n1 + 1))),1);
set Sp = { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } ;
set Sn = { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } ;
A20: { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } c= Sphere ((0. (TOP-REAL (n1 + 1))),1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } or x in Sphere ((0. (TOP-REAL (n1 + 1))),1) )
assume x in { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } ; :: thesis: x in Sphere ((0. (TOP-REAL (n1 + 1))),1)
then consider s being Point of (TOP-REAL (n1 + 1)) such that
A21: x = s and
s . (n1 + 1) >= 0 and
A22: |.s.| = 1 ;
s - (0. (TOP-REAL (n1 + 1))) = s by RLVECT_1:13;
hence x in Sphere ((0. (TOP-REAL (n1 + 1))),1) by A22, A21; :: thesis: verum

end;

A23: [#] ((TOP-REAL n) | (cl_Ball (p,r))) = cl_Ball (p,r) by PRE_TOPC:def 5;
reconsider Spr = Sphere (p,r) as Subset of ((TOP-REAL n) | (cl_Ball (p,r))) by A23, TOPREAL9:17;
A24: ( cl_Ball ((0. (TOP-REAL (n1 + 1))),1) is compact & not cl_Ball ((0. (TOP-REAL (n1 + 1))),1) is boundary ) by Lm2;
( cl_Ball (p,r) is compact & not cl_Ball (p,r) is boundary ) by Lm2, A10;
then consider h being Function of ((TOP-REAL n) | (cl_Ball (p,r))),((TOP-REAL (n1 + 1)) | (cl_Ball ((0. (TOP-REAL (n1 + 1))),1))) such that
A25: h is being_homeomorphism and
A26: h .: (Fr (cl_Ball (p,r))) = Fr (cl_Ball ((0. (TOP-REAL (n1 + 1))),1)) by A24, BROUWER2:7;
A27: ind Spr = ind (h .: Spr) by A25, METRIZTS:3, TOPDIM_1:27;
A28: { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } c= Sphere ((0. (TOP-REAL (n1 + 1))),1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } or x in Sphere ((0. (TOP-REAL (n1 + 1))),1) )
assume x in { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } ; :: thesis: x in Sphere ((0. (TOP-REAL (n1 + 1))),1)
then consider s being Point of (TOP-REAL (n1 + 1)) such that
A29: x = s and
s . (n1 + 1) <= 0 and
A30: |.s.| = 1 ;
s - (0. (TOP-REAL (n1 + 1))) = s by RLVECT_1:13;
hence x in Sphere ((0. (TOP-REAL (n1 + 1))),1) by A30, A29; :: thesis: verum

end;

then reconsider Sp = { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } , Sn = { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } as Subset of (TOP-REAL (n1 + 1)) by A20, XBOOLE_1:1;
A31: Sphere ((0. (TOP-REAL (n1 + 1))),1) c= Sp \/ Sn

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Sphere ((0. (TOP-REAL (n1 + 1))),1) or x in Sp \/ Sn )
assume A32: x in Sphere ((0. (TOP-REAL (n1 + 1))),1) ; :: thesis: x in Sp \/ Sn
then reconsider x = x as Point of (TOP-REAL (n1 + 1)) ;
A33: ( x . (n1 + 1) >= 0 or x . (n1 + 1) <= 0 ) ;
|.x.| = 1 by A32, TOPREAL9:12;
then ( x in Sp or x in Sn ) by A33;
hence x in Sp \/ Sn by XBOOLE_0:def 3; :: thesis: verum

end;

A34: Sn = { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) } ;
then A35: Sp is closed by Th2;
A36: Sp = { s where s is Point of (TOP-REAL (n1 + 1)) : ( s . (n1 + 1) >= 0 & |.s.| = 1 ) } ;
A37: ( Sp, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic & Sn, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic )

proof

set TD = Tdisk ((0. (TOP-REAL n1)),1);
deffunc H₁( Nat) -> Element of K10(K11( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)) = PROJ ((n1 + 1),$1);
consider FF being FinSequence such that
A38: ( len FF = n1 & ( for k being Nat st k in dom FF holds
FF . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng FF c= Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng FF or x in Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1) )
assume x in rng FF ; :: thesis: x in Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)
then consider i being object such that
A39: i in dom FF and
A40: FF . i = x by FUNCT_1:def 3;
reconsider i = i as Nat by A39;
H₁(i) in Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1) by FUNCT_2:8;
hence x in Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1) by A38, A39, A40; :: thesis: verum

end;

then reconsider FF = FF as FinSequence of Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1) by FINSEQ_1:def 4;
reconsider FF = FF as Element of n1 -tuples_on (Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)) by A38, FINSEQ_2:92;
set FFF = <:FF:>;
A41: [#] (Tdisk ((0. (TOP-REAL n1)),1)) = cl_Ball ((0. (TOP-REAL n1)),1) by PRE_TOPC:def 5;
<:FF:> .: Sp = cl_Ball ((0. (TOP-REAL n1)),1) by A38, Th1, A34;
then A42: rng (<:FF:> | Sp) c= the carrier of (Tdisk ((0. (TOP-REAL n1)),1)) by RELAT_1:115, A41;
A43: dom <:FF:> = the carrier of (TOP-REAL (n1 + 1)) by FUNCT_2:def 1;
then Sn /\ (dom <:FF:>) = Sn by XBOOLE_1:28;
then A44: dom (<:FF:> | Sn) = Sn by RELAT_1:61;
Sp /\ (dom <:FF:>) = Sp by A43, XBOOLE_1:28;
then A45: dom (<:FF:> | Sp) = Sp by RELAT_1:61;
[#] ((TOP-REAL (n1 + 1)) | Sp) = Sp by PRE_TOPC:def 5;
then reconsider Fsp = <:FF:> | Sp as Function of ((TOP-REAL (n1 + 1)) | Sp),(Tdisk ((0. (TOP-REAL n1)),1)) by A42, A45, FUNCT_2:2;
A46: [#] ((TOP-REAL (n1 + 1)) | Sn) = Sn by PRE_TOPC:def 5;
<:FF:> .: Sn = cl_Ball ((0. (TOP-REAL n1)),1) by A38, Th1, A36;
then rng (<:FF:> | Sn) c= the carrier of (Tdisk ((0. (TOP-REAL n1)),1)) by RELAT_1:115, A41;
then reconsider Fsn = <:FF:> | Sn as Function of ((TOP-REAL (n1 + 1)) | Sn),(Tdisk ((0. (TOP-REAL n1)),1)) by A46, FUNCT_2:2, A44;
A47: Fsn is being_homeomorphism by A38, Th1, A36;
Fsp is being_homeomorphism by A38, Th1, A34;
hence ( Sp, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic & Sn, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic ) by A47, T_0TOPSP:def 1, METRIZTS:def 1; :: thesis: verum

end;

A48: ind (cl_Ball ((0. (TOP-REAL n1)),1)) = n1 by Lm2, Th6;
then A49: ind Sp = n1 by A37, TOPDIM_1:27;
Sp c= Sp \/ Sn by XBOOLE_1:7;
then A50: n1 <= ind (Sp \/ Sn) by A49, TOPDIM_1:19;
ind Sn = n1 by A37, A48, TOPDIM_1:27;
then ind (Sp \/ Sn) <= n1 by A35, A49, A1;
then A51: ind (Sp \/ Sn) = n1 by A50, XXREAL_0:1;
Fr (cl_Ball (p,r)) = Sphere (p,r) by BROUWER2:5, A10;
then h .: Spr = Sphere ((0. (TOP-REAL (n1 + 1))),1) by A26, BROUWER2:5;
then A52: ind (h .: Spr) = ind (Sphere ((0. (TOP-REAL (n1 + 1))),1)) by TOPDIM_1:21;
Sp \/ Sn c= Sphere ((0. (TOP-REAL (n1 + 1))),1) by A20, A28, XBOOLE_1:8;
then ind (Sphere ((0. (TOP-REAL (n1 + 1))),1)) = n1 by A31, XBOOLE_0:def 10, A51;
hence ind (Sphere (p,r)) = n - 1 by TOPDIM_1:21, A52, A27; :: thesis: verum

end;

end;