set L = Closed-Interval-TSpace (0,1);
let UL be Subset-Family of (Tunit_circle 2); :: thesis:
assume that
A1: UL is Cover of (Tunit_circle 2) and
A2: UL is open ; :: thesis:
let Y be non empty TopSpace; :: thesis:
let F be continuous Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis:
let y be Point of Y; :: thesis:
A3: [#] (Tunit_circle 2) = union UL by A1, SETFAM_1:45;
A4: for i being Point of I[01] ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,i] in U & U in UL )

proof

let i be Point of I[01]; :: thesis:
consider U being set such that
A5: ( F . [y,i] in U & U in UL ) by A3, TARSKI:def 4;
reconsider U = U as non empty open Subset of (Tunit_circle 2) by A2, A5;
take U ; :: thesis:
thus ( F . [y,i] in U & U in UL ) by A5; :: thesis:

end;

then ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,0[01]] in U & U in UL ) ;
then reconsider UL1 = UL as non empty set ;
set C = the carrier of Y;
defpred S₁[ set , set ] means ex V being open Subset of (Tunit_circle 2) st
( V in UL1 & F . [y,$1] in V & $2 = V );
A6: for i being Element of the carrier of I[01] ex z being Element of UL1 st S₁[i,z]

proof

let i be Element of the carrier of I[01]; :: thesis:
ex U being non empty open Subset of (Tunit_circle 2) st
( F . [y,i] in U & U in UL ) by A4;
hence ex z being Element of UL1 st S₁[i,z] ; :: thesis:

end;

consider I0 being Function of the carrier of I[01],UL1 such that
A7: for i being Element of the carrier of I[01] holds S₁[i,I0 . i] from FUNCT_2:sch 3(A6);
defpred S₂[ object , object ] means ex M being open Subset of Y ex O being open connected Subset of I[01] st
( y in M & $1 in O & F .: [:M,O:] c= I0 . $1 & $2 = [:M,O:] );
A8: for i being Element of the carrier of I[01] ex z being Subset of [: the carrier of Y, the carrier of I[01]:] st S₂[i,z]

proof

let i be Element of the carrier of I[01]; :: thesis:
consider V being open Subset of (Tunit_circle 2) such that
V in UL1 and
A9: F . [y,i] in V and
A10: I0 . i = V by A7;
consider W being Subset of [:Y,I[01]:] such that
A11: [y,i] in W and
A12: W is open and
A13: F .: W c= V by A9, JGRAPH_2:10;
consider Q being Subset-Family of [:Y,I[01]:] such that
A14: W = union Q and
A15: for e being set st e in Q holds
ex A being Subset of Y ex B being Subset of I[01] st
( e = [:A,B:] & A is open & B is open ) by A12, BORSUK_1:5;
consider Z being set such that
A16: [y,i] in Z and
A17: Z in Q by A11, A14, TARSKI:def 4;
consider A being Subset of Y, B being Subset of I[01] such that
A18: Z = [:A,B:] and
A19: A is open and
A20: B is open by A15, A17;
reconsider A = A as open Subset of Y by A19;
A21: i in B by A16, A18, ZFMISC_1:87;
reconsider B = B as non empty open Subset of I[01] by A16, A18, A20;
reconsider i1 = i as Point of (I[01] | B) by A21, PRE_TOPC:8;
Component_of i1 is a_component by CONNSP_1:40;
then A22: Component_of i1 is open by CONNSP_2:15;
Component_of (i,B) = Component_of i1 by A21, CONNSP_3:def 7;
then reconsider D = Component_of (i,B) as open connected Subset of I[01] by A21, A22, CONNSP_3:33, TSEP_1:17;
reconsider z = [:A,D:] as Subset of [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2;
take z ; :: thesis:
take A ; :: thesis:
take D ; :: thesis:
thus y in A by A16, A18, ZFMISC_1:87; :: thesis:
thus i in D by A21, CONNSP_3:26; :: thesis:
D c= B by A21, Th3;
then A23: z c= [:A,B:] by ZFMISC_1:95;
[:A,B:] c= W by A14, A17, A18, ZFMISC_1:74;
then z c= W by A23;
then F .: z c= F .: W by RELAT_1:123;
hence F .: [:A,D:] c= I0 . i by A10, A13; :: thesis:
thus z = [:A,D:] ; :: thesis:

end;

consider I1 being Function of the carrier of I[01],(bool [: the carrier of Y, the carrier of I[01]:]) such that
A24: for i being Element of the carrier of I[01] holds S₂[i,I1 . i] from FUNCT_2:sch 3(A8);
reconsider C1 = rng I1 as Subset-Family of [:Y,I[01]:] by BORSUK_1:def 2;
A25: C1 is open

proof

let P be Subset of [:Y,I[01]:]; :: according to TOPS_2:def 1 :: thesis:
assume P in C1 ; :: thesis:
then consider i being object such that
A26: i in dom I1 and
A27: I1 . i = P by FUNCT_1:def 3;
S₂[i,I1 . i] by A24, A26;
hence P is open by A27, BORSUK_1:6; :: thesis:

end;

A28: dom I1 = the carrier of I[01] by FUNCT_2:def 1;
[:{y},([#] I[01]):] c= union C1

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in [:{y},([#] I[01]):] ; :: thesis:
then consider a1, a2 being object such that
A29: a1 in {y} and
A30: a2 in [#] I[01] and
A31: a = [a1,a2] by ZFMISC_1:def 2;
A32: a1 = y by A29, TARSKI:def 1;
reconsider a2 = a2 as Point of I[01] by A30;
consider M being open Subset of Y, O being open connected Subset of I[01] such that
A33: ( y in M & a2 in O ) and
F .: [:M,O:] c= I0 . a2 and
A34: I1 . a2 = [:M,O:] by A24;
( [y,a2] in [:M,O:] & [:M,O:] in C1 ) by A28, A33, A34, FUNCT_1:def 3, ZFMISC_1:87;
hence a in union C1 by A31, A32, TARSKI:def 4; :: thesis:

end;

then A35: C1 is Cover of [:{y},([#] I[01]):] by SETFAM_1:def 11;
[:{y},([#] I[01]):] is compact by BORSUK_3:23;
then consider G being Subset-Family of [:Y,I[01]:] such that
A36: G c= C1 and
A37: G is Cover of [:{y},([#] I[01]):] and
A38: G is finite by A35, A25;
set NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ;
{ M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } c= bool the carrier of Y

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } ; :: thesis:
then ex M being open Subset of Y st
( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;
hence a in bool the carrier of Y ; :: thesis:

end;

then reconsider NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I[01] st [:M,O:] in G ) } as Subset-Family of Y ;
consider p being Function such that
A39: rng p = G and
A40: dom p in omega by A38, FINSET_1:def 1;
defpred S₃[ object , object ] means ex M being open Subset of Y ex O being non empty open Subset of I[01] st
( y in M & p . $1 = [:M,O:] & $2 = M );
A41: for x being object st x in dom p holds
ex y being object st
( y in NN & S₃[x,y] )

proof

let x be object ; :: thesis:
assume x in dom p ; :: thesis:
then A42: p . x in rng p by FUNCT_1:def 3;
then consider i being object such that
A43: i in dom I1 and
A44: I1 . i = p . x by A36, A39, FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01] such that
A45: ( y in M & i in O ) and
F .: [:M,O:] c= I0 . i and
A46: I1 . i = [:M,O:] by A24, A43;
take M ; :: thesis:
thus ( M in NN & S₃[x,M] ) by A39, A42, A44, A45, A46; :: thesis:

end;

consider p1 being Function of (dom p),NN such that
A47: for x being object st x in dom p holds
S₃[x,p1 . x] from FUNCT_2:sch 1(A41);
set ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ;
A48: [:{y},([#] I[01]):] c= union G by A37, SETFAM_1:def 11;
A49: y in {y} by TARSKI:def 1;
then [y,0[01]] in [:{y},([#] I[01]):] by ZFMISC_1:def 2;
then consider Z being set such that
[y,0[01]] in Z and
A50: Z in G by A48, TARSKI:def 4;
consider i being object such that
A51: i in dom I1 and
A52: I1 . i = Z by A36, A50, FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01] such that
A53: y in M and
i in O and
F .: [:M,O:] c= I0 . i and
A54: I1 . i = [:M,O:] by A24, A51;
A55: M in NN by A50, A52, A53, A54;
then A56: dom p1 = dom p by FUNCT_2:def 1;
rng p1 = NN

proof

thus rng p1 c= NN ; :: according to XBOOLE_0:def 10 :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in NN ; :: thesis:
then consider M being open Subset of Y such that
A57: a = M and
y in M and
A58: ex O being open Subset of I[01] st [:M,O:] in G ;
consider O being open Subset of I[01] such that
A59: [:M,O:] in G by A58;
consider b being object such that
A60: b in dom p and
A61: p . b = [:M,O:] by A39, A59, FUNCT_1:def 3;
consider M1 being open Subset of Y, O1 being non empty open Subset of I[01] such that
A62: ( y in M1 & p . b = [:M1,O1:] ) and
A63: p1 . b = M1 by A47, A60;
M1 = M by A61, A62, ZFMISC_1:110;
hence a in rng p1 by A56, A57, A60, A63, FUNCT_1:def 3; :: thesis:

end;

then A64: NN is finite by A40, A56, FINSET_1:def 1;
NN is open

proof

let a be Subset of Y; :: according to TOPS_2:def 1 :: thesis:
assume a in NN ; :: thesis:
then ex M being open Subset of Y st
( a = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;
hence a is open ; :: thesis:

end;

then reconsider N = meet NN as open Subset of Y by A64, TOPS_2:20;
{ O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I[01]

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } ; :: thesis:
then ex O being open connected Subset of I[01] st
( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence a in bool the carrier of I[01] ; :: thesis:

end;

then reconsider ICOV = { O where O is open connected Subset of I[01] : ex M being open Subset of Y st [:M,O:] in G } as Subset-Family of (Closed-Interval-TSpace (0,1)) by TOPMETR:20;
[#] (Closed-Interval-TSpace (0,1)) c= union ICOV

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in [#] (Closed-Interval-TSpace (0,1)) ; :: thesis:
then reconsider a = a as Point of I[01] by TOPMETR:20;
[y,a] in [:{y},([#] I[01]):] by A49, ZFMISC_1:def 2;
then consider Z being set such that
A65: [y,a] in Z and
A66: Z in G by A48, TARSKI:def 4;
consider i being object such that
A67: i in dom I1 and
A68: I1 . i = Z by A36, A66, FUNCT_1:def 3;
consider M being open Subset of Y, O being open connected Subset of I[01] such that
y in M and
i in O and
F .: [:M,O:] c= I0 . i and
A69: I1 . i = [:M,O:] by A24, A67;
( a in O & O in ICOV ) by A65, A66, A68, A69, ZFMISC_1:87;
hence a in union ICOV by TARSKI:def 4; :: thesis:

end;

then A70: ICOV is Cover of (Closed-Interval-TSpace (0,1)) by SETFAM_1:def 11;
set NCOV = the IntervalCover of ICOV;
set T = the IntervalCoverPts of the IntervalCover of ICOV;
A71: ICOV is connected

proof

let X be Subset of (Closed-Interval-TSpace (0,1)); :: according to RCOMP_3:def 1 :: thesis:
assume X in ICOV ; :: thesis:
then ex O being open connected Subset of I[01] st
( X = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence X is connected by TOPMETR:20; :: thesis:

end;

A72: ICOV is open

proof

let a be Subset of (Closed-Interval-TSpace (0,1)); :: according to TOPS_2:def 1 :: thesis:
assume a in ICOV ; :: thesis:
then ex O being open connected Subset of I[01] st
( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence a is open by TOPMETR:20; :: thesis:

end;

then reconsider T = the IntervalCoverPts of the IntervalCover of ICOV as non empty FinSequence of REAL by A70, A71, Lm15;
take T ; :: thesis:
thus ( T . 1 = 0 & T . (len T) = 1 ) by A70, A72, A71, RCOMP_3:def 3; :: thesis:
thus T is increasing by A70, A72, A71, RCOMP_3:65; :: thesis:
take N ; :: thesis:

now :: thesis:

let Z be set ; :: thesis:
assume Z in NN ; :: thesis:
then ex M being open Subset of Y st
( Z = M & y in M & ex O being open Subset of I[01] st [:M,O:] in G ) ;
hence y in Z ; :: thesis:

end;

hence y in N by A55, SETFAM_1:def 1; :: thesis:
let i be Nat; :: thesis:
assume that
A73: i in dom T and
A74: i + 1 in dom T ; :: thesis:
A75: 1 <= i by A73, FINSEQ_3:25;
A76: i + 1 <= len T by A74, FINSEQ_3:25;
len T = (len the IntervalCover of ICOV) + 1 by A70, A72, A71, RCOMP_3:def 3;
then i <= len the IntervalCover of ICOV by A76, XREAL_1:6;
then i in dom the IntervalCover of ICOV by A75, FINSEQ_3:25;
then A77: the IntervalCover of ICOV . i in rng the IntervalCover of ICOV by FUNCT_1:def 3;
rng the IntervalCover of ICOV c= ICOV by A70, A72, A71, RCOMP_3:def 2;
then the IntervalCover of ICOV . i in ICOV by A77;
then consider O being open connected Subset of I[01] such that
A78: the IntervalCover of ICOV . i = O and
A79: ex M being open Subset of Y st [:M,O:] in G ;
consider M being open Subset of Y such that
A80: [:M,O:] in G by A79;
i < len T by A76, NAT_1:13;
then A81: [.(T . i),(T . (i + 1)).] c= O by A70, A72, A71, A75, A78, RCOMP_3:66;
consider j being object such that
A82: j in dom I1 and
A83: I1 . j = [:M,O:] by A36, A80, FUNCT_1:def 3;
consider V being open Subset of (Tunit_circle 2) such that
A84: V in UL1 and
A85: F . [y,j] in V and
A86: I0 . j = V by A7, A82;
reconsider V = V as non empty open Subset of (Tunit_circle 2) by A85;
take V ; :: thesis:
thus V in UL by A84; :: thesis:
consider M1 being open Subset of Y, O1 being open connected Subset of I[01] such that
A87: y in M1 and
A88: j in O1 and
A89: F .: [:M1,O1:] c= I0 . j and
A90: I1 . j = [:M1,O1:] by A24, A82;
M = M1 by A83, A87, A88, A90, ZFMISC_1:110;
then M in NN by A80, A87;
then N c= M by SETFAM_1:3;
then [:N,[.(T . i),(T . (i + 1)).]:] c= [:M1,O1:] by A83, A90, A81, ZFMISC_1:96;
then F .: [:N,[.(T . i),(T . (i + 1)).]:] c= F .: [:M1,O1:] by RELAT_1:123;
hence F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V by A89, A86; :: thesis: