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 Def2;
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 A24: (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
A25: xp in R1 \ {(C `)} by A2, TARSKI:def 4;
A26: 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 A27: x in C ; :: thesis:
then reconsider p = x as Point of M ;
take I = Int (W . p); :: thesis:
A28: Int (W . p) c= W . p by TOPS_1:16;
W . p in rng W by A16, FUNCT_1:def 3;
then A29: W . p is connected by A7;
A30: 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 A28, A27, XBOOLE_0:3;
then W . p c= C by A1, A29, CONNSP_3:16, A26;
hence ( I is open & I c= C & x in I ) by A30, CONNSP_2:def 1, A28; :: 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:
A31: R1 \ {(C `)} c= R1 by XBOOLE_1:36;
A32: 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
A33: x in y and
A34: y in R1 \ {(C `)} by TARSKI:def 4;
y in R1 by A34, ZFMISC_1:56;
then ( y in IntW or y = C ` ) by A21, ZFMISC_1:136;
then consider U being Subset of M such that
A35: y = Int U and
A36: U in rng (W | C) by A34, ZFMISC_1:56;
A37: U is connected by A32, A36, A7;
A38: Int U c= U by TOPS_1:16;
consider p being object such that
A39: p in dom (W | C) and
A40: (W | C) . p = U by A36, FUNCT_1:def 3;
A41: W . p = U by A39, A40, FUNCT_1:47;
p in dom W by A39, RELAT_1:57;
then reconsider p = p as Point of M ;
U is a_neighborhood of p by A4, A41;
then p in Int U by CONNSP_2:def 1;
then W . p meets C by A38, A39, A41, XBOOLE_0:3;
then U c= C by A41, A1, A37, CONNSP_3:16, A26;
hence x in C by A38, A33, A35; :: thesis:

end;

then A42: union (R1 \ {(C `)}) = C by A24, TOPS_2:4;
A43: 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 A44: x in R1 \ {(C `)} ; :: thesis:
then A45: x <> C ` by ZFMISC_1:56;
x in R1 by A44, ZFMISC_1:56;
then x in IntW by A21, A45, ZFMISC_1:136;
then consider U being Subset of M such that
A46: x = Int U and
A47: U in rng (W | C) ;
consider y being object such that
A48: y in dom (W | C) and
A49: (W | C) . y = U by A47, FUNCT_1:def 3;
take y ; :: thesis:
thus y in C by A48; :: thesis:
let A be Subset of M; :: thesis:
thus ( A = W . y implies Int A = x ) by A48, FUNCT_1:47, A46, A49; :: thesis:

end;

consider cc being Function such that
A50: ( dom cc = R1 \ {(C `)} & ( for x being object st x in R1 \ {(C `)} holds
S₂[x,cc . x] ) ) from CLASSES1:sch 1(A43);
S₂[xp,cc . xp] by A25, A50;
then reconsider cp = cc . xp as Point of M ;
consider n being Nat such that
A51: 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 ) ) );
A52: Int (W . cp) = xp by A25, A50;
A53: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

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

per cases ;

suppose k > 0 ; :: thesis:

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

proof

reconsider UWR3 = union (W .: (cc .: R3)) as connected Subset of M by A58;
A86: Int (W . c2) c= W . c2 by TOPS_1:16;
c1 in cc .: R3 by A77, A57, A50, FUNCT_1:def 6;
then A87: W . c1 in W .: (cc .: R3) by A16, FUNCT_1:def 6;
Int (W . c1) c= W . c1 by TOPS_1:16;
then A88: m in UWR3 by A87, A85, A76, TARSKI:def 4;
UWR3 c= Cl UWR3 by PRE_TOPC:18;
then Cl UWR3 meets W . c2 by A86, A81, A78, A88, XBOOLE_0:3;
then A89: not UWR3,W . c2 are_separated by CONNSP_1:def 1;
cc .: R4 = (cc .: R3) \/ (cc .: {m2}) by A81, RELAT_1:120
.= (cc .: R3) \/ (Im (cc,m2)) by RELAT_1:def 16
.= (cc .: R3) \/ {(cc . m2)} by FUNCT_1:59, A82, A50 ;
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 A90: union (W .: (cc .: R4)) = UWR3 \/ (union {(W . c2)}) by ZFMISC_1:78
.= UWR3 \/ (W . c2) by ZFMISC_1:25 ;
W . c2 is connected by A84, A7;
hence union (W .: (cc .: R4)) is connected Subset of M by A89, CONNSP_1:17, A90; :: thesis:

end;

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

per cases by A91, ZFMISC_1:136;

suppose a in R3 ; :: thesis:

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

end;

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

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

end;

suppose A96: k = 0 ; :: thesis:

reconsider R3 = {(Int (W . cp))} as Subset-Family of M ;
take R3 ; :: thesis:
thus card R3 = k + 1 by A96, CARD_1:30; :: thesis:
thus A97: R3 c= R1 \ {(C `)} by A52, A25, ZFMISC_1:31; :: thesis:
cc .: R3 = Im (cc,xp) by A52, RELAT_1:def 16
.= {cp} by FUNCT_1:59, A25, A50 ;
then W .: (cc .: R3) = Im (W,cp) by RELAT_1:def 16
.= {(W . cp)} by A16, FUNCT_1:59 ;
then A98: 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 A98, A7; :: thesis:
let a, b be Subset of M; :: thesis:
assume that
A99: a in R3 and
A100: b = W . (cc . a) ; :: thesis:
S₂[a,cc . a] by A99, A97, A50;
then reconsider ca = cc . a as Point of M ;
Int (W . cp) = xp by A25, A50;
hence M | b, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A51, TARSKI:def 1, A99, A100; :: thesis:

end;

take n ; :: thesis:
A101: 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(A101, A53);
then S₃[ card (R1 \ {(C `)})] ;
then consider R3 being Subset-Family of M such that
A102: card R3 = card (R1 \ {(C `)}) and
A103: R3 c= R1 \ {(C `)} and
A104: 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 ;
A105: R1 \ {(C `)} = R3 by A102, A103, 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:
A106: [#] MC = C by PRE_TOPC:def 5;
then consider y being set such that
A107: q in y and
A108: y in R1 \ {(C `)} by A42, TARSKI:def 4;
S₂[y,cc . y] by A50, A108;
then reconsider c = cc . y as Point of M ;
reconsider Wc = W . c as Subset of M ;
A109: 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 A110: Wc is connected by A7;
A111: Int Wc = y by A50, A108;
then Wc meets C by A109, A107, A106, XBOOLE_0:3;
then A112: Wc c= C by A110, A1, CONNSP_3:16, A26;
then (W . c) /\ C = W . c by XBOOLE_1:28;
then A113: Down (Wc,C) = W . c by CONNSP_3:def 5;
(Int Wc) /\ C = Int Wc by A112, A109, 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, A107, A111, A113, A109, TOPS_1:22;
then A114: Down (Wc,C) is a_neighborhood of q by CONNSP_2:def 1;
M | (W . c) = (M | C) | (Down (Wc,C)) by A113, A106, PRE_TOPC:7;
hence ex U being a_neighborhood of q st MC | U, Tdisk ((0. (TOP-REAL n)),1) are_homeomorphic by A114, A104, A105, A108; :: thesis:

end;

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