let M be non empty compact locally_euclidean TopSpace; :: thesis:
defpred S₁[ Point of M, Subset of M] means ( $2 is a_neighborhood of $1 & ex n being Nat st M | $2, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic );
let C be Subset of M; :: thesis:
assume A1: C is a_component ; :: thesis:
consider p being object such that
A2: p in C by A1, XBOOLE_0:def 1;
reconsider p = p as Point of M by A2;
A3: for x being Point of M ex y being Element of bool the carrier of M st S₁[x,y]

let x be Point of M; :: thesis:
ex U being a_neighborhood of x ex n being Nat st M | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by Def1;
hence ex y being Element of bool the carrier of M st S₁[x,y] ; :: thesis:

end;

consider W being Function of M,(bool the carrier of M) such that
A4: for x being Point of M holds S₁[x,W . x] from FUNCT_2:sch 3(A3);
reconsider MC = M | C as non empty connected TopSpace by A1, CONNSP_1:def 3;
defpred S₂[ object , object ] means ( $2 in C & ( for A being Subset of M st A = W . $2 holds
Int A = $1 ) );
set IntW = { (Int U) where U is Subset of M : U in rng (W | C) } ;
{ (Int U) where U is Subset of M : U in rng (W | C) } c= bool the carrier of M

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (Int U) where U is Subset of M : U in rng (W | C) } ; :: thesis:
then ex U being Subset of M st
( x = Int U & U in rng (W | C) ) ;
hence x in bool the carrier of M ; :: thesis:

end;

then reconsider IntW = { (Int U) where U is Subset of M : U in rng (W | C) } as Subset-Family of M ;
reconsider R = IntW \/ {(C `)} as Subset-Family of M ;
for A being Subset of M st A in R holds
A is open

proof

let A be Subset of M; :: thesis:
assume A5: A in R ; :: thesis:

per cases by ZFMISC_1:136, A5;

suppose A = C ` ; :: thesis:

hence A is open by A1; :: thesis:

end;

suppose A in IntW ; :: thesis:

then ex U being Subset of M st
( A = Int U & U in rng (W | C) ) ;
hence A is open ; :: thesis:

end;

then A6: R is open by TOPS_2:def 1;
A7: for A being Subset of M st A in rng W holds
( A is connected & not Int A is empty )

proof

let A be Subset of M; :: thesis:
assume A in rng W ; :: thesis:
then consider p being object such that
A8: p in dom W and
A9: W . p = A by FUNCT_1:def 3;
consider n being Nat such that
A10: M | A, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A8, A9, A4;
reconsider AA = A as non empty Subset of M by A8, A9, A4;
A11: Tdisk ((0. (TOP-REAL n)),1) is connected by CONNSP_1:def 3;
Tdisk ((0. (TOP-REAL n)),1),M | AA are_homeomorphic by A10;
then consider h being Function of (Tdisk ((0. (TOP-REAL n)),1)),(M | A) such that
A12: h is being_homeomorphism by T_0TOPSP:def 1;
reconsider p = p as Point of M by A8;
A13: S₁[p,A] by A8, A9, A4;
A14: rng h = [#] (M | A) by A12, TOPS_2:def 5;
A15: h .: (dom h) = rng h by RELAT_1:113;
dom h = [#] (Tdisk ((0. (TOP-REAL n)),1)) by A12, TOPS_2:def 5;
then M | A is connected by A15, A14, A12, A11, CONNSP_1:14;
hence ( A is connected & not Int A is empty ) by CONNSP_1:def 3, A13, CONNSP_2:def 1; :: thesis:

end;

A16: dom W = the carrier of M by FUNCT_2:def 1;
the carrier of M c= union R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in the carrier of M ; :: thesis:
then reconsider x = x as Point of M ;

per cases ;

suppose x in C ; :: thesis:

then A17: x in dom (W | C) by RELAT_1:57, A16;
then A18: (W | C) . x = W . x by FUNCT_1:47;
(W | C) . x in rng (W | C) by A17, FUNCT_1:def 3;
then Int (W . x) in IntW by A18;
then A19: Int (W . x) in R by XBOOLE_0:def 3;
W . x is a_neighborhood of x by A4;
then x in Int (W . x) by CONNSP_2:def 1;
hence x in union R by A19, TARSKI:def 4; :: thesis:

end;

suppose not x in C ; :: thesis:

then x in ([#] M) \ C by XBOOLE_0:def 5;
then A20: x in C ` by SUBSET_1:def 4;
C ` in R by ZFMISC_1:136;
hence x in union R by A20, TARSKI:def 4; :: thesis:

end;

then consider R1 being Subset-Family of M such that
A21: R1 c= R and
A22: R1 is Cover of M and
A23: R1 is finite by SETFAM_1:def 11, A6, COMPTS_1:def 1;
reconsider R1 = R1 as finite Subset-Family of M by A23;
set R2 = R1 \ {(C `)};
union R1 = the carrier of M by A22, SETFAM_1:45;
then WW: (union R1) \ (union {(C `)}) = the carrier of M \ (C `) by ZFMISC_1:25
.= (C `) ` by SUBSET_1:def 4
.= C ;
then C c= union (R1 \ {(C `)}) by TOPS_2:4;
then consider xp being set such that
p in xp and
A26: xp in R1 \ {(C `)} by A2, TARSKI:def 4;
A27: C = Component_of C by A1, CONNSP_3:7;
for x being set holds
( x in C iff ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) )

proof

let x be set ; :: thesis:

hereby :: thesis:

assume A28: x in C ; :: thesis:
then reconsider p = x as Point of M ;
take I = Int (W . p); :: thesis:
A29: Int (W . p) c= W . p by TOPS_1:16;
W . p in rng W by A16, FUNCT_1:def 3;
then A30: W . p is connected by A7;
A31: W . p is a_neighborhood of p by A4;
then p in Int (W . p) by CONNSP_2:def 1;
then W . p meets C by A29, A28, XBOOLE_0:3;
then W . p c= C by A1, A30, CONNSP_3:16, A27;
hence ( I is open & I c= C & x in I ) by A31, CONNSP_2:def 1, A29; :: thesis:

end;

thus ( ex Q being Subset of M st
( Q is open & Q c= C & x in Q ) implies x in C ) ; :: thesis:

end;

hence C is open by TOPS_1:25; :: thesis:
A32: R1 \ {(C `)} c= R1 by XBOOLE_1:36;
A33: rng (W | C) c= rng W by RELAT_1:70;
union (R1 \ {(C `)}) c= C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in union (R1 \ {(C `)}) ; :: thesis:
then consider y being set such that
A34: x in y and
A35: y in R1 \ {(C `)} by TARSKI:def 4;
y in R1 by A35, ZFMISC_1:56;
then ( y in IntW or y = C ` ) by A21, ZFMISC_1:136;
then consider U being Subset of M such that
A36: y = Int U and
A37: U in rng (W | C) by A35, ZFMISC_1:56;
A38: U is connected by A33, A37, A7;
A39: Int U c= U by TOPS_1:16;
consider p being object such that
A41: p in dom (W | C) and
A42: (W | C) . p = U by A37, FUNCT_1:def 3;
A43: W . p = U by A41, A42, FUNCT_1:47;
p in dom W by A41, RELAT_1:57;
then reconsider p = p as Point of M ;
U is a_neighborhood of p by A4, A43;
then p in Int U by CONNSP_2:def 1;
then W . p meets C by A39, A41, A43, XBOOLE_0:3;
then U c= C by A43, A1, A38, CONNSP_3:16, A27;
hence x in C by A39, A34, A36; :: thesis:

end;

then A44: union (R1 \ {(C `)}) = C by WW, TOPS_2:4;
A45: for x being object st x in R1 \ {(C `)} holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis:
assume A46: x in R1 \ {(C `)} ; :: thesis:
then A47: x <> C ` by ZFMISC_1:56;
x in R1 by A46, ZFMISC_1:56;
then x in IntW by A21, A47, ZFMISC_1:136;
then consider U being Subset of M such that
A48: x = Int U and
A49: U in rng (W | C) ;
consider y being object such that
A50: y in dom (W | C) and
A51: (W | C) . y = U by A49, FUNCT_1:def 3;
take y ; :: thesis:
thus y in C by A50; :: thesis:
let A be Subset of M; :: thesis:
thus ( A = W . y implies Int A = x ) by A50, FUNCT_1:47, A48, A51; :: thesis:

end;

consider cc being Function such that
A52: ( dom cc = R1 \ {(C `)} & ( for x being object st x in R1 \ {(C `)} holds
S₂[x,cc . x] ) ) from CLASSES1:sch 1(A45);
S₂[xp,cc . xp] by A26, A52;
then reconsider cp = cc . xp as Point of M ;
consider n being Nat such that
A53: M | (W . cp), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A4;
defpred S₃[ Nat] means ( $1 <= card (R1 \ {(C `)}) implies ex R3 being Subset-Family of M st
( card R3 = $1 & R3 c= R1 \ {(C `)} & union (W .: (cc .: R3)) is connected Subset of M & ( for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ) ) );
A54: Int (W . cp) = xp by A26, A52;
A55: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume A56: S₃[k] ; :: thesis:
assume A57: k + 1 <= card (R1 \ {(C `)}) ; :: thesis:
then consider R3 being Subset-Family of M such that
A58: card R3 = k and
A59: R3 c= R1 \ {(C `)} and
A60: union (W .: (cc .: R3)) is connected Subset of M and
A61: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by NAT_1:13, A56;
k < card (R1 \ {(C `)}) by A57, NAT_1:13;
then k in Segm (card (R1 \ {(C `)})) by NAT_1:44;
then (R1 \ {(C `)}) \ R3 <> {} by A58, CARD_1:68;
then consider r23 being object such that
A62: r23 in (R1 \ {(C `)}) \ R3 by XBOOLE_0:def 1;
reconsider r23 = r23 as set by TARSKI:1;
A63: r23 in R1 \ {(C `)} by A62, XBOOLE_0:def 5;
then A64: r23 <> C ` by ZFMISC_1:56;
r23 in R1 by A63, ZFMISC_1:56;
then r23 in IntW by A21, A64, ZFMISC_1:136;
then A65: ex B being Subset of M st
( Int B = r23 & B in rng (W | C) ) ;
A66: r23 c= union ((R1 \ {(C `)}) \ R3) by A62, ZFMISC_1:74;

per cases ;

suppose k > 0 ; :: thesis:

then not R3 is empty by A58;
then consider r3 being set such that
A67: r3 in R3 ;
A68: r3 <> C ` by A59, A67, ZFMISC_1:56;
r3 in R1 by A59, A67, ZFMISC_1:56;
then r3 in IntW by A21, A68, ZFMISC_1:136;
then A69: ex A being Subset of M st
( Int A = r3 & A in rng (W | C) ) ;
r3 c= union R3 by A67, ZFMISC_1:74;
then reconsider U3 = union R3 as non empty Subset of M by A33, A69, A7;
set A1 = the Subset of M;
reconsider U23 = union ((R1 \ {(C `)}) \ R3) as Subset of M ;
set D2 = Down (U3,C);
set D23 = Down (U23,C);
Down (U3,C) = U3 /\ C by CONNSP_3:def 5;
then A70: Down (U3,C) = U3 by XBOOLE_1:28, A44, A59, ZFMISC_1:77;
((R1 \ {(C `)}) \ R3) \/ R3 = (R1 \ {(C `)}) \/ R3 by XBOOLE_1:39
.= R1 \ {(C `)} by A59, XBOOLE_1:12 ;
then U3 \/ U23 = C by A44, ZFMISC_1:78;
then A71: U3 \/ U23 = [#] MC by PRE_TOPC:def 5;
R3 c= R1 by A32, A59;
then R3 is open by A21, XBOOLE_1:1, A6, TOPS_2:11;
then A72: Down (U3,C) is open by TOPS_2:19, CONNSP_3:28;
A73: (R1 \ {(C `)}) \ R3 c= R1 \ {(C `)} by XBOOLE_1:36;
then (R1 \ {(C `)}) \ R3 c= R1 by A32;
then (R1 \ {(C `)}) \ R3 is open by A21, XBOOLE_1:1, A6, TOPS_2:11;
then A74: Down (U23,C) is open by TOPS_2:19, CONNSP_3:28;
Down (U23,C) = U23 /\ C by CONNSP_3:def 5;
then A75: Down (U23,C) = U23 by XBOOLE_1:28, A73, A44, ZFMISC_1:77;
U23 <> {} MC by A66, A33, A65, A7;
then consider m being object such that
A76: m in U3 and
A77: m in U23 by A72, A74, A70, A75, A71, CONNSP_1:11, XBOOLE_0:3;
consider m1 being set such that
A78: m in m1 and
A79: m1 in R3 by A76, TARSKI:def 4;
S₂[m1,cc . m1] by A59, A79, A52;
then reconsider c1 = cc . m1 as Point of M ;
consider m2 being set such that
A80: m in m2 and
A81: m2 in (R1 \ {(C `)}) \ R3 by A77, TARSKI:def 4;
A82: m2 in R1 \ {(C `)} by A81, XBOOLE_0:def 5;
then S₂[m2,cc . m2] by A52;
then reconsider c2 = cc . m2 as Point of M ;
set R4 = R3 \/ {(Int (W . c2))};
R3 is finite by A58;
then reconsider R4 = R3 \/ {(Int (W . c2))} as finite Subset-Family of M ;
take R4 ; :: thesis:
A83: Int (W . c2) = m2 by A82, A52;
then not Int (W . c2) in R3 by A81, XBOOLE_0:def 5;
hence card R4 = k + 1 by A58, A59, CARD_2:41; :: thesis:
A84: m2 in R1 \ {(C `)} by A81, XBOOLE_0:def 5;
then {m2} c= R1 \ {(C `)} by ZFMISC_1:31;
hence A85: R4 c= R1 \ {(C `)} by A83, A59, XBOOLE_1:8; :: thesis:
A86: W . c2 in rng W by A16, FUNCT_1:def 3;
A87: Int (W . c1) = m1 by A59, A79, A52;
thus union (W .: (cc .: R4)) is connected Subset of M :: thesis:

proof

reconsider UWR3 = union (W .: (cc .: R3)) as connected Subset of M by A60;
A88: Int (W . c2) c= W . c2 by TOPS_1:16;
c1 in cc .: R3 by A79, A59, A52, FUNCT_1:def 6;
then A89: W . c1 in W .: (cc .: R3) by A16, FUNCT_1:def 6;
Int (W . c1) c= W . c1 by TOPS_1:16;
then A90: m in UWR3 by A89, A87, A78, TARSKI:def 4;
UWR3 c= Cl UWR3 by PRE_TOPC:18;
then Cl UWR3 meets W . c2 by A88, A83, A80, A90, XBOOLE_0:3;
then A91: not UWR3,W . c2 are_separated by CONNSP_1:def 1;
cc .: R4 = (cc .: R3) \/ (cc .: {m2}) by A83, RELAT_1:120
.= (cc .: R3) \/ (Im (cc,m2)) by RELAT_1:def 16
.= (cc .: R3) \/ {(cc . m2)} by FUNCT_1:59, A84, A52 ;
then W .: (cc .: R4) = (W .: (cc .: R3)) \/ (W .: {c2}) by RELAT_1:120
.= (W .: (cc .: R3)) \/ (Im (W,c2)) by RELAT_1:def 16
.= (W .: (cc .: R3)) \/ {(W . c2)} by A16, FUNCT_1:59 ;
then A92: union (W .: (cc .: R4)) = UWR3 \/ (union {(W . c2)}) by ZFMISC_1:78
.= UWR3 \/ (W . c2) by ZFMISC_1:25 ;
W . c2 is connected by A86, A7;
hence union (W .: (cc .: R4)) is connected Subset of M by A91, CONNSP_1:17, A92; :: thesis:

end;

let a, b be Subset of M; :: thesis:
assume that
A93: a in R4 and
A94: b = W . (cc . a) ; :: thesis:

per cases by A93, ZFMISC_1:136;

suppose a in R3 ; :: thesis:

hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A94, A61; :: thesis:

end;

suppose a = Int (W . c2) ; :: thesis:

then Int b = Int (W . c2) by A82, A52, A94;
then A95: m in Int b by A82, A52, A80;
S₂[a,cc . a] by A93, A85, A52;
then reconsider ca = cc . a as Point of M ;
A96: M | (W . c1), Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A79, A61;
S₁[ca,W . ca] by A4;
then consider mm being Nat such that
A97: M | b, Tdisk ((0. (TOP-REAL mm)),1) are_homeomorphic by A94;
Int (W . c1) = m1 by A59, A79, A52;
then n = mm by A96, A78, A95, XBOOLE_0:3, A97, BROUWER3:14;
hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A97; :: thesis:

end;

suppose A98: k = 0 ; :: thesis:

reconsider R3 = {(Int (W . cp))} as Subset-Family of M ;
take R3 ; :: thesis:
thus card R3 = k + 1 by A98, CARD_1:30; :: thesis:
thus A99: R3 c= R1 \ {(C `)} by A54, A26, ZFMISC_1:31; :: thesis:
cc .: R3 = Im (cc,xp) by A54, RELAT_1:def 16
.= {cp} by FUNCT_1:59, A26, A52 ;
then W .: (cc .: R3) = Im (W,cp) by RELAT_1:def 16
.= {(W . cp)} by A16, FUNCT_1:59 ;
then A100: union (W .: (cc .: R3)) = W . cp by ZFMISC_1:25;
W . cp in rng W by A16, FUNCT_1:def 3;
hence union (W .: (cc .: R3)) is connected Subset of M by A100, A7; :: thesis:
let a, b be Subset of M; :: thesis:
assume that
A101: a in R3 and
A102: b = W . (cc . a) ; :: thesis:
S₂[a,cc . a] by A101, A99, A52;
then reconsider ca = cc . a as Point of M ;
Int (W . cp) = xp by A26, A52;
hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A53, TARSKI:def 1, A101, A102; :: thesis:

end;

take n ; :: thesis:
A105: S₃[ 0 ]

proof

set R3 = the empty Subset of (bool the carrier of M);
assume 0 <= card (R1 \ {(C `)}) ; :: thesis:
take the empty Subset of (bool the carrier of M) ; :: thesis:
thus ( card the empty Subset of (bool the carrier of M) = 0 & the empty Subset of (bool the carrier of M) c= R1 \ {(C `)} ) ; :: thesis:
reconsider UR3 = union (W .: (cc .: the empty Subset of (bool the carrier of M))) as empty Subset of M by ZFMISC_1:2;
UR3 is connected ;
hence union (W .: (cc .: the empty Subset of (bool the carrier of M))) is connected Subset of M ; :: thesis:
let A, B be Subset of M; :: thesis:
thus ( A in the empty Subset of (bool the carrier of M) & B = W . (cc . A) implies M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ) ; :: thesis:

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(A105, A55);
then S₃[ card (R1 \ {(C `)})] ;
then consider R3 being Subset-Family of M such that
A106: card R3 = card (R1 \ {(C `)}) and
A107: R3 c= R1 \ {(C `)} and
A108: for A, B being Subset of M st A in R3 & B = W . (cc . A) holds
M | B, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic ;
A109: R1 \ {(C `)} = R3 by A106, A107, CARD_2:102;
for p being Point of MC ex U being a_neighborhood of p st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic

proof

let q be Point of MC; :: thesis:
A110: [#] MC = C by PRE_TOPC:def 5;
then consider y being set such that
A111: q in y and
A112: y in R1 \ {(C `)} by A44, TARSKI:def 4;
S₂[y,cc . y] by A52, A112;
then reconsider c = cc . y as Point of M ;
reconsider Wc = W . c as Subset of M ;
A113: Int Wc c= Wc by TOPS_1:16;
set D = Down (Wc,C);
set DI = Down ((Int Wc),C);
Wc in rng W by A16, FUNCT_1:def 3;
then A114: Wc is connected by A7;
A115: Int Wc = y by A52, A112;
then Wc meets C by A113, A111, A110, XBOOLE_0:3;
then A116: Wc c= C by A114, A1, CONNSP_3:16, A27;
then (W . c) /\ C = W . c by XBOOLE_1:28;
then A117: Down (Wc,C) = W . c by CONNSP_3:def 5;
(Int Wc) /\ C = Int Wc by A116, A113, XBOOLE_1:1, XBOOLE_1:28;
then Down ((Int Wc),C) = Int Wc by CONNSP_3:def 5;
then q in Int (Down (Wc,C)) by CONNSP_3:28, A111, A115, A117, A113, TOPS_1:22;
then A118: Down (Wc,C) is a_neighborhood of q by CONNSP_2:def 1;
M | (W . c) = (M | C) | (Down (Wc,C)) by A117, A110, PRE_TOPC:7;
hence ex U being a_neighborhood of q st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A118, A108, A109, A112; :: thesis:

end;

hence M | C is non empty n -locally_euclidean TopSpace by Def2; :: thesis: