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

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

assume A10:
r > 0
; :: thesis: ind (Sphere (p,r)) = n - 1
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;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

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

end;

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

then A12:
p = 0. (TOP-REAL n)
by EUCLID:77;

Sphere (p,r) = {}

end;Sphere (p,r) = {}

proof

hence
ind (Sphere (p,r)) = n - 1
by TOPDIM_1:6, A11; :: thesis: verum
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;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

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

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)

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)

A31: Sphere ((0. (TOP-REAL (n1 + 1))),1) c= Sp \/ Sn

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 )

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

A23:
[#] ((TOP-REAL n) | (cl_Ball (p,r))) = cl_Ball (p,r)
by PRE_TOPC:def 5;
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;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

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

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

A31: Sphere ((0. (TOP-REAL (n1 + 1))),1) c= Sp \/ Sn

proof

A34:
Sn = { t where t is Point of (TOP-REAL (n1 + 1)) : ( t . (n1 + 1) <= 0 & |.t.| = 1 ) }
;
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;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

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

A48:
ind (cl_Ball ((0. (TOP-REAL n1)),1)) = n1
by Lm2, Th6;
set TD = Tdisk ((0. (TOP-REAL n1)),1);

deffunc H_{1}( 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_{1}(k) ) )
from FINSEQ_1:sch 2();

rng FF c= Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)

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;deffunc H

consider FF being FinSequence such that

A38: ( len FF = n1 & ( for k being Nat st k in dom FF holds

FF . k = H

rng FF c= Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1)

proof

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;
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_{1}(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;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

hence x in Funcs ( the carrier of (TOP-REAL (n1 + 1)), the carrier of R^1) by A38, A39, A40; :: thesis: verum

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

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