let n be Nat; :: thesis: for p being Point of ()
for r being Real st r > 0 holds
ind (Sphere (p,r)) = n - 1

let p be Point of (); :: 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 () 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 () st ind A <= i & ind B <= i & A is closed holds
ind (A \/ B) <= i

let A, B be Subset of (); :: thesis: ( ind A <= i & ind B <= i & A is closed implies ind (A \/ B) <= i )
set TT = TopStruct(# the carrier of (), the topology of () #);
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 (), the topology of () #) ;
A5: a is closed by ;
A6: TopStruct(# the carrier of (), the topology of () #) | AB is second-countable ;
A7: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
A8: TopStruct(# the carrier of (), the topology of () #) = () | ([#] ()) by TSEP_1:93;
then A9: ind b <= i by ;
ind a <= i by ;
then ind AB <= i by A9, A5, A8, A7, A6, TOPDIM_2:5;
hence ind (A \/ B) <= i by ; :: 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. () 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 () by A13;
x = 0. () by
.= 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 ; :: 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 ;
card {|[(u - r)]|} = 1 by CARD_1:30;
then ind {|[(u - r)]|} = 0 by ;
then A18: ind ({|[(u - r)]|} \/ {|[(u + r)]|}) = 0 by A17, A15, A1;
{<*(u - r)*>,<*(u + r)*>} = Fr (Ball (p,r)) by
.= Sphere (p,r) by ;
hence ind (Sphere (p,r)) = n - 1 by ; :: 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 ; :: thesis: verum
end;
A23: [#] (() | (cl_Ball (p,r))) = cl_Ball (p,r) by PRE_TOPC:def 5;
reconsider Spr = Sphere (p,r) as Subset of (() | (cl_Ball (p,r))) by ;
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 ;
then consider h being Function of (() | (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 ;
A27: ind Spr = ind (h .: Spr) by ;
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 ; :: 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 ;
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 ;
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 H1( 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 = H1(k) ) ) from 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;
H1(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 ; :: 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 ;
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 ;
then A42: rng (<:FF:> | Sp) c= the carrier of (Tdisk ((0. (TOP-REAL n1)),1)) by ;
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 ;
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 ;
A46: [#] ((TOP-REAL (n1 + 1)) | Sn) = Sn by PRE_TOPC:def 5;
<:FF:> .: Sn = cl_Ball ((0. (TOP-REAL n1)),1) by ;
then rng (<:FF:> | Sn) c= the carrier of (Tdisk ((0. (TOP-REAL n1)),1)) by ;
then reconsider Fsn = <:FF:> | Sn as Function of ((TOP-REAL (n1 + 1)) | Sn),(Tdisk ((0. (TOP-REAL n1)),1)) by ;
A47: Fsn is being_homeomorphism by ;
Fsp is being_homeomorphism by ;
hence ( Sp, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic & Sn, cl_Ball ((0. (TOP-REAL n1)),1) are_homeomorphic ) by ; :: thesis: verum
end;
A48: ind (cl_Ball ((0. (TOP-REAL n1)),1)) = n1 by ;
then A49: ind Sp = n1 by ;
Sp c= Sp \/ Sn by XBOOLE_1:7;
then A50: n1 <= ind (Sp \/ Sn) by ;
ind Sn = n1 by ;
then ind (Sp \/ Sn) <= n1 by A35, A49, A1;
then A51: ind (Sp \/ Sn) = n1 by ;
Fr (cl_Ball (p,r)) = Sphere (p,r) by ;
then h .: Spr = Sphere ((0. (TOP-REAL (n1 + 1))),1) by ;
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 ;
then ind (Sphere ((0. (TOP-REAL (n1 + 1))),1)) = n1 by ;
hence ind (Sphere (p,r)) = n - 1 by ; :: thesis: verum
end;
end;