set L = Closed-Interval-TSpace (0,1);
let UL be Subset-Family of (); :: thesis: ( UL is Cover of () & UL is open implies for Y being non empty TopSpace
for F being continuous Function of ,()
for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) ) )

assume that
A1: UL is Cover of () and
A2: UL is open ; :: thesis: for Y being non empty TopSpace
for F being continuous Function of ,()
for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let Y be non empty TopSpace; :: thesis: for F being continuous Function of ,()
for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let F be continuous Function of ,(); :: thesis: for y being Point of Y ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

let y be Point of Y; :: thesis: ex T being non empty FinSequence of REAL st
( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

A3: [#] () = union UL by ;
A4: for i being Point of I ex U being non empty open Subset of () st
( F . [y,i] in U & U in UL )
proof
let i be Point of I; :: thesis: ex U being non empty open Subset of () st
( F . [y,i] in U & U in UL )

consider U being set such that
A5: ( F . [y,i] in U & U in UL ) by ;
reconsider U = U as non empty open Subset of () by A2, A5;
take U ; :: thesis: ( F . [y,i] in U & U in UL )
thus ( F . [y,i] in U & U in UL ) by A5; :: thesis: verum
end;
then ex U being non empty open Subset of () st
( F . [y,0] in U & U in UL ) ;
then reconsider UL1 = UL as non empty set ;
set C = the carrier of Y;
defpred S1[ set , set ] means ex V being open Subset of () st
( V in UL1 & F . [y,\$1] in V & \$2 = V );
A6: for i being Element of the carrier of I ex z being Element of UL1 st S1[i,z]
proof
let i be Element of the carrier of I; :: thesis: ex z being Element of UL1 st S1[i,z]
ex U being non empty open Subset of () st
( F . [y,i] in U & U in UL ) by A4;
hence ex z being Element of UL1 st S1[i,z] ; :: thesis: verum
end;
consider I0 being Function of the carrier of I,UL1 such that
A7: for i being Element of the carrier of I holds S1[i,I0 . i] from defpred S2[ object , object ] means ex M being open Subset of Y ex O being open connected Subset of I 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 ex z being Subset of [: the carrier of Y, the carrier of I:] st S2[i,z]
proof
let i be Element of the carrier of I; :: thesis: ex z being Subset of [: the carrier of Y, the carrier of I:] st S2[i,z]
consider V being open Subset of () such that
V in UL1 and
A9: F . [y,i] in V and
A10: I0 . i = V by A7;
consider W being Subset of such that
A11: [y,i] in W and
A12: W is open and
A13: F .: W c= V by ;
consider Q being Subset-Family of 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 st
( e = [:A,B:] & A is open & B is open ) by ;
consider Z being set such that
A16: [y,i] in Z and
A17: Z in Q by ;
consider A being Subset of Y, B being Subset of I such that
A18: Z = [:A,B:] and
A19: A is open and
A20: B is open by ;
reconsider A = A as open Subset of Y by A19;
A21: i in B by ;
reconsider B = B as non empty open Subset of I by ;
reconsider i1 = i as Point of () by ;
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 ;
then reconsider D = Component_of (i,B) as open connected Subset of I by ;
reconsider z = [:A,D:] as Subset of [: the carrier of Y, the carrier of I:] by BORSUK_1:def 2;
take z ; :: thesis: S2[i,z]
take A ; :: thesis: ex O being open connected Subset of I st
( y in A & i in O & F .: [:A,O:] c= I0 . i & z = [:A,O:] )

take D ; :: thesis: ( y in A & i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )
thus y in A by ; :: thesis: ( i in D & F .: [:A,D:] c= I0 . i & z = [:A,D:] )
thus i in D by ; :: thesis: ( F .: [:A,D:] c= I0 . i & z = [:A,D:] )
D c= B by ;
then A23: z c= [:A,B:] by ZFMISC_1:95;
[:A,B:] c= W by ;
then z c= W by A23;
then F .: z c= F .: W by RELAT_1:123;
hence F .: [:A,D:] c= I0 . i by ; :: thesis: z = [:A,D:]
thus z = [:A,D:] ; :: thesis: verum
end;
consider I1 being Function of the carrier of I,(bool [: the carrier of Y, the carrier of I:]) such that
A24: for i being Element of the carrier of I holds S2[i,I1 . i] from reconsider C1 = rng I1 as Subset-Family of by BORSUK_1:def 2;
A25: C1 is open
proof
let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in C1 or P is open )
assume P in C1 ; :: thesis: P is open
then consider i being object such that
A26: i in dom I1 and
A27: I1 . i = P by FUNCT_1:def 3;
S2[i,I1 . i] by ;
hence P is open by ; :: thesis: verum
end;
A28: dom I1 = the carrier of I by FUNCT_2:def 1;
[:{y},():] c= union C1
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [:{y},():] or a in union C1 )
assume a in [:{y},():] ; :: thesis: a in union C1
then consider a1, a2 being object such that
A29: a1 in {y} and
A30: a2 in [#] I and
A31: a = [a1,a2] by ZFMISC_1:def 2;
A32: a1 = y by ;
reconsider a2 = a2 as Point of I by A30;
consider M being open Subset of Y, O being open connected Subset of I 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 ;
hence a in union C1 by ; :: thesis: verum
end;
then A35: C1 is Cover of [:{y},():] by SETFAM_1:def 11;
[:{y},():] is compact by BORSUK_3:23;
then consider G being Subset-Family of such that
A36: G c= C1 and
A37: G is Cover of [:{y},():] and
A38: G is finite by ;
set NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I st [:M,O:] in G ) } ;
{ M where M is open Subset of Y : ( y in M & ex O being open Subset of I st [:M,O:] in G ) } c= bool the carrier of Y
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I st [:M,O:] in G ) } or a in bool the carrier of Y )
assume a in { M where M is open Subset of Y : ( y in M & ex O being open Subset of I st [:M,O:] in G ) } ; :: thesis: a in bool the carrier of Y
then ex M being open Subset of Y st
( a = M & y in M & ex O being open Subset of I st [:M,O:] in G ) ;
hence a in bool the carrier of Y ; :: thesis: verum
end;
then reconsider NN = { M where M is open Subset of Y : ( y in M & ex O being open Subset of I 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 ;
defpred S3[ object , object ] means ex M being open Subset of Y ex O being non empty open Subset of I 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 & S3[x,y] )
proof
let x be object ; :: thesis: ( x in dom p implies ex y being object st
( y in NN & S3[x,y] ) )

assume x in dom p ; :: thesis: ex y being object st
( y in NN & S3[x,y] )

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 ;
consider M being open Subset of Y, O being open connected Subset of I such that
A45: ( y in M & i in O ) and
F .: [:M,O:] c= I0 . i and
A46: I1 . i = [:M,O:] by ;
take M ; :: thesis: ( M in NN & S3[x,M] )
thus ( M in NN & S3[x,M] ) by A39, A42, A44, A45, A46; :: thesis: verum
end;
consider p1 being Function of (dom p),NN such that
A47: for x being object st x in dom p holds
S3[x,p1 . x] from set ICOV = { O where O is open connected Subset of I : ex M being open Subset of Y st [:M,O:] in G } ;
A48: [:{y},():] c= union G by ;
A49: y in {y} by TARSKI:def 1;
then [y,0] in [:{y},():] by ZFMISC_1:def 2;
then consider Z being set such that
[y,0] in Z and
A50: Z in G by ;
consider i being object such that
A51: i in dom I1 and
A52: I1 . i = Z by ;
consider M being open Subset of Y, O being open connected Subset of I such that
A53: y in M and
i in O and
F .: [:M,O:] c= I0 . i and
A54: I1 . i = [:M,O:] by ;
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: NN c= rng p1
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in NN or a in rng p1 )
assume a in NN ; :: thesis: a in rng p1
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 st [:M,O:] in G ;
consider O being open Subset of I 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 ;
consider M1 being open Subset of Y, O1 being non empty open Subset of I such that
A62: ( y in M1 & p . b = [:M1,O1:] ) and
A63: p1 . b = M1 by ;
M1 = M by ;
hence a in rng p1 by ; :: thesis: verum
end;
then A64: NN is finite by ;
NN is open
proof
let a be Subset of Y; :: according to TOPS_2:def 1 :: thesis: ( not a in NN or a is open )
assume a in NN ; :: thesis: a is open
then ex M being open Subset of Y st
( a = M & y in M & ex O being open Subset of I st [:M,O:] in G ) ;
hence a is open ; :: thesis: verum
end;
then reconsider N = meet NN as open Subset of Y by ;
{ O where O is open connected Subset of I : ex M being open Subset of Y st [:M,O:] in G } c= bool the carrier of I
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { O where O is open connected Subset of I : ex M being open Subset of Y st [:M,O:] in G } or a in bool the carrier of I )
assume a in { O where O is open connected Subset of I : ex M being open Subset of Y st [:M,O:] in G } ; :: thesis: a in bool the carrier of I
then ex O being open connected Subset of I st
( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence a in bool the carrier of I ; :: thesis: verum
end;
then reconsider ICOV = { O where O is open connected Subset of I : ex M being open Subset of Y st [:M,O:] in G } as Subset-Family of () by TOPMETR:20;
[#] () c= union ICOV
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [#] () or a in union ICOV )
assume a in [#] () ; :: thesis: a in union ICOV
then reconsider a = a as Point of I by TOPMETR:20;
[y,a] in [:{y},():] by ;
then consider Z being set such that
A65: [y,a] in Z and
A66: Z in G by ;
consider i being object such that
A67: i in dom I1 and
A68: I1 . i = Z by ;
consider M being open Subset of Y, O being open connected Subset of I such that
y in M and
i in O and
F .: [:M,O:] c= I0 . i and
A69: I1 . i = [:M,O:] by ;
( a in O & O in ICOV ) by ;
hence a in union ICOV by TARSKI:def 4; :: thesis: verum
end;
then A70: ICOV is Cover of () 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 (); :: according to RCOMP_3:def 1 :: thesis: ( not X in ICOV or X is connected )
assume X in ICOV ; :: thesis: X is connected
then ex O being open connected Subset of I st
( X = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence X is connected by TOPMETR:20; :: thesis: verum
end;
A72: ICOV is open
proof
let a be Subset of (); :: according to TOPS_2:def 1 :: thesis: ( not a in ICOV or a is open )
assume a in ICOV ; :: thesis: a is open
then ex O being open connected Subset of I st
( a = O & ex M being open Subset of Y st [:M,O:] in G ) ;
hence a is open by TOPMETR:20; :: thesis: verum
end;
then reconsider T = the IntervalCoverPts of the IntervalCover of ICOV as non empty FinSequence of REAL by ;
take T ; :: thesis: ( T . 1 = 0 & T . (len T) = 1 & T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus ( T . 1 = 0 & T . (len T) = 1 ) by ; :: thesis: ( T is increasing & ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) ) )

thus T is increasing by ; :: thesis: ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

take N ; :: thesis: ( y in N & ( for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) ) )

now :: thesis: for Z being set st Z in NN holds
y in Z
let Z be set ; :: thesis: ( Z in NN implies y in Z )
assume Z in NN ; :: thesis: y in Z
then ex M being open Subset of Y st
( Z = M & y in M & ex O being open Subset of I st [:M,O:] in G ) ;
hence y in Z ; :: thesis: verum
end;
hence y in N by ; :: thesis: for i being Nat st i in dom T & i + 1 in dom T holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

let i be Nat; :: thesis: ( i in dom T & i + 1 in dom T implies ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui ) )

assume that
A73: i in dom T and
A74: i + 1 in dom T ; :: thesis: ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= Ui )

A75: 1 <= i by ;
A76: i + 1 <= len T by ;
len T = (len the IntervalCover of ICOV) + 1 by ;
then i <= len the IntervalCover of ICOV by ;
then i in dom the IntervalCover of ICOV by ;
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 ;
then the IntervalCover of ICOV . i in ICOV by A77;
then consider O being open connected Subset of I 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 ;
then A81: [.(T . i),(T . (i + 1)).] c= O by ;
consider j being object such that
A82: j in dom I1 and
A83: I1 . j = [:M,O:] by ;
consider V being open Subset of () such that
A84: V in UL1 and
A85: F . [y,j] in V and
A86: I0 . j = V by ;
reconsider V = V as non empty open Subset of () by A85;
take V ; :: thesis: ( V in UL & F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V )
thus V in UL by A84; :: thesis: F .: [:N,[.(T . i),(T . (i + 1)).]:] c= V
consider M1 being open Subset of Y, O1 being open connected Subset of I 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 ;
M = M1 by ;
then M in NN by ;
then N c= M by SETFAM_1:3;
then [:N,[.(T . i),(T . (i + 1)).]:] c= [:M1,O1:] by ;
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 ; :: thesis: verum