consider UL being Subset-Family of () such that
A1: ( UL is Cover of () & UL is open ) and
A2: for U being Subset of () st U in UL holds
ex D being mutually-disjoint open Subset-Family of R^1 st
( union D = CircleMap " U & ( for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),(() | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by Lm13;
let Y be non empty TopSpace; :: thesis: for F being Function of ,()
for Ft being Function of [:Y,():],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,:] = CircleMap * Ft holds
ex G being Function of ,R^1 st
( G is continuous & F = CircleMap * G & G | [: the carrier of Y,:] = Ft & ( for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,:] = Ft holds
G = H ) )

let F be Function of ,(); :: thesis: for Ft being Function of [:Y,():],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,:] = CircleMap * Ft holds
ex G being Function of ,R^1 st
( G is continuous & F = CircleMap * G & G | [: the carrier of Y,:] = Ft & ( for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,:] = Ft holds
G = H ) )

let Ft be Function of [:Y,():],R^1; :: thesis: ( F is continuous & Ft is continuous & F | [: the carrier of Y,:] = CircleMap * Ft implies ex G being Function of ,R^1 st
( G is continuous & F = CircleMap * G & G | [: the carrier of Y,:] = Ft & ( for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,:] = Ft holds
G = H ) ) )

assume that
A3: F is continuous and
A4: Ft is continuous and
A5: F | [: the carrier of Y,:] = CircleMap * Ft ; :: thesis: ex G being Function of ,R^1 st
( G is continuous & F = CircleMap * G & G | [: the carrier of Y,:] = Ft & ( for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,:] = Ft holds
G = H ) )

defpred S1[ set , set ] means ex y being Point of Y ex t being Point of I[01] ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( \$1 = [y,t] & \$2 = Fn . \$1 & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) );
A6: dom F = the carrier of by FUNCT_2:def 1
.= [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2 ;
A7: the carrier of [:Y,():] = [: the carrier of Y, the carrier of ():] by BORSUK_1:def 2;
then A8: dom Ft = [: the carrier of Y,:] by ;
A9: for x being Point of ex z being Point of R^1 st S1[x,z]
proof
let x be Point of ; :: thesis: ex z being Point of R^1 st S1[x,z]
consider y being Point of Y, t being Point of I[01] such that
A10: x = [y,t] by BORSUK_1:10;
consider TT being non empty FinSequence of REAL such that
A11: TT . 1 = 0 and
A12: TT . (len TT) = 1 and
A13: TT is increasing and
A14: ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom TT & i + 1 in dom TT holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) ) ) by A3, A1, Th21;
consider N being open Subset of Y such that
A15: y in N and
A16: for i being Nat st i in dom TT & i + 1 in dom TT holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) by A14;
reconsider N = N as non empty open Subset of Y by A15;
defpred S2[ Nat] means ( \$1 in dom TT implies ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . \$1).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] ) );
A17: len TT in dom TT by FINSEQ_5:6;
A18: 1 in dom TT by FINSEQ_5:6;
A19: now :: thesis: for i being Element of NAT st i in dom TT holds
( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
let i be Element of NAT ; :: thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) )
assume A20: i in dom TT ; :: thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
1 <= i by ;
then ( 1 = i or 1 < i ) by XXREAL_0:1;
hence A21: 0 <= TT . i by ; :: thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) )
assume A22: i + 1 in dom TT ; :: thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
A23: i + 0 < i + 1 by XREAL_1:8;
hence A24: TT . i < TT . (i + 1) by ; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
i + 1 <= len TT by ;
then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1;
hence TT . (i + 1) <= 1 by ; :: thesis: ( TT . i < 1 & 0 < TT . (i + 1) )
hence TT . i < 1 by ; :: thesis: 0 < TT . (i + 1)
thus 0 < TT . (i + 1) by ; :: thesis: verum
end;
A25: now :: thesis: for i being Nat st 0 <= TT . i & TT . (i + 1) <= 1 holds
[.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
let i be Nat; :: thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] )
assume that
A26: 0 <= TT . i and
A27: TT . (i + 1) <= 1 ; :: thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] )
assume A28: a in [.(TT . i),(TT . (i + 1)).] ; :: thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
a <= TT . (i + 1) by ;
then A29: a <= 1 by ;
0 <= a by ;
hence a in the carrier of I[01] by ; :: thesis: verum
end;
end;
A30: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume that
A31: S2[i] and
A32: i + 1 in dom TT ; :: thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )

per cases ( i = 0 or i in dom TT ) by ;
suppose A33: i = 0 ; :: thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )

take N2 = N; :: thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )

set Fn = Ft | [:N2,:];
set S = [.0,(TT . (i + 1)).];
A34: [.0,(TT . (i + 1)).] = by ;
reconsider S = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by ;
A35: dom (Ft | [:N2,:]) = [:N2,S:] by ;
reconsider K0 = [:N2,S:] as non empty Subset of [:Y,():] by ;
A36: ( the carrier of [:(Y | N2),():] = [: the carrier of (Y | N2), the carrier of ():] & rng (Ft | [:N2,:]) c= the carrier of R^1 ) by BORSUK_1:def 2;
( the carrier of (Y | N2) = N2 & the carrier of () = S ) by PRE_TOPC:8;
then reconsider Fn = Ft | [:N2,:] as Function of [:(Y | N2),():],R^1 by ;
A37: dom (F | [:N2,S:]) = [:N2,S:] by ;
reconsider S1 = S as non empty Subset of () by ;
take S ; :: thesis: ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )

take Fn ; :: thesis: ( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )
thus S = [.0,(TT . (i + 1)).] ; :: thesis: ( y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )
thus y in N2 by A15; :: thesis: ( N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )
thus N2 c= N ; :: thesis: ( Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )
I[01] | S = Sspace 0[01] by
.= () | S1 by ;
then [:(Y | N2),():] = [:Y,():] | K0 by BORSUK_3:22;
hence Fn is continuous by ; :: thesis: ( F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )
rng Fn c= dom CircleMap by ;
then A38: dom () = dom Fn by RELAT_1:27;
A39: [:N2,S:] c= dom Ft by ;
for x being object st x in dom (F | [:N2,S:]) holds
(F | [:N2,S:]) . x = () . x
proof
let x be object ; :: thesis: ( x in dom (F | [:N2,S:]) implies (F | [:N2,S:]) . x = () . x )
assume A40: x in dom (F | [:N2,S:]) ; :: thesis: (F | [:N2,S:]) . x = () . x
thus (F | [:N2,S:]) . x = F . x by
.= () . x by
.= CircleMap . (Ft . x) by
.= CircleMap . (Fn . x) by
.= () . x by ; :: thesis: verum
end;
hence F | [:N2,S:] = CircleMap * Fn by ; :: thesis: Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:]
A41: dom (Fn | [: the carrier of Y,:]) = [:N2,S:] /\ [: the carrier of Y,:] by ;
A42: for x being object st x in dom (Fn | [: the carrier of Y,:]) holds
(Fn | [: the carrier of Y,:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x
proof
A43: [:N2,:] c= [:N2, the carrier of I[01]:] by ;
let x be object ; :: thesis: ( x in dom (Fn | [: the carrier of Y,:]) implies (Fn | [: the carrier of Y,:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x )
assume A44: x in dom (Fn | [: the carrier of Y,:]) ; :: thesis: (Fn | [: the carrier of Y,:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x
A45: x in [:N2,:] by ;
x in [: the carrier of Y,:] by ;
hence (Fn | [: the carrier of Y,:]) . x = Fn . x by FUNCT_1:49
.= Ft . x by
.= (Ft | [:N2, the carrier of I[01]:]) . x by ;
:: thesis: verum
end;
dom (Ft | [:N2, the carrier of I[01]:]) = [: the carrier of Y,:] /\ [:N2, the carrier of I[01]:] by
.= [:N2,S:] by ;
hence Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] by ; :: thesis: verum
end;
suppose A46: i in dom TT ; :: thesis: ex N2 being non empty open Subset of Y ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N2),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N2 & N2 c= N & Fn is continuous & F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] )

set SS = [.(TT . i),(TT . (i + 1)).];
consider Ui being non empty Subset of () such that
A47: Ui in UL and
A48: F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui by ;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A49: union D = CircleMap " Ui and
A50: for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),(() | Ui) st f = CircleMap | d holds
f is being_homeomorphism by ;
A51: the carrier of (() | Ui) = Ui by PRE_TOPC:8;
A52: TT . i < TT . (i + 1) by ;
then TT . i in [.(TT . i),(TT . (i + 1)).] by XXREAL_1:1;
then A53: [y,(TT . i)] in [:N,[.(TT . i),(TT . (i + 1)).]:] by ;
consider N2 being open Subset of Y, S being non empty Subset of I[01], Fn being Function of [:(Y | N2),():],R^1 such that
A54: S = [.0,(TT . i).] and
A55: y in N2 and
A56: N2 c= N and
A57: Fn is continuous and
A58: F | [:N2,S:] = CircleMap * Fn and
A59: Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] by ;
reconsider N2 = N2 as non empty open Subset of Y by A55;
A60: the carrier of [:(Y | N2),():] = [: the carrier of (Y | N2), the carrier of ():] by BORSUK_1:def 2;
N2 c= N2 ;
then reconsider N7 = N2 as non empty Subset of (Y | N2) by PRE_TOPC:8;
A61: dom Fn = the carrier of [:(Y | N2),():] by FUNCT_2:def 1;
A62: 0 <= TT . i by ;
then A63: TT . i in S by ;
then reconsider Ti = {(TT . i)} as non empty Subset of I[01] by ZFMISC_1:31;
A64: the carrier of () = S by PRE_TOPC:8;
then reconsider Ti2 = Ti as non empty Subset of () by ;
set FnT = Fn | [:N2,Ti:];
A65: ( the carrier of [:(Y | N2),(I[01] | Ti):] = [: the carrier of (Y | N2), the carrier of (I[01] | Ti):] & rng (Fn | [:N2,Ti:]) c= REAL ) by ;
A66: [:N2,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] by ;
A67: the carrier of (Y | N2) = N2 by PRE_TOPC:8;
{(TT . i)} c= S by ;
then A68: dom (Fn | [:N2,Ti:]) = [:N2,{(TT . i)}:] by ;
A69: [:((Y | N2) | N7),(() | Ti2):] = [:(Y | N2),():] | [:N7,Ti2:] by BORSUK_3:22;
A70: the carrier of (I[01] | Ti) = Ti by PRE_TOPC:8;
then reconsider FnT = Fn | [:N2,Ti:] as Function of [:(Y | N2),(I[01] | Ti):],R^1 by ;
( (Y | N2) | N7 = Y | N2 & () | Ti2 = I[01] | Ti ) by GOBOARD9:2;
then A71: FnT is continuous by ;
A72: Fn . [y,(TT . i)] in REAL by XREAL_0:def 1;
[y,(TT . i)] in dom F by ;
then A73: F . [y,(TT . i)] in F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by ;
A74: [y,(TT . i)] in [:N2,S:] by ;
then F . [y,(TT . i)] = () . [y,(TT . i)] by
.= CircleMap . (Fn . [y,(TT . i)]) by ;
then Fn . [y,(TT . i)] in CircleMap " Ui by ;
then consider Uit being set such that
A75: Fn . [y,(TT . i)] in Uit and
A76: Uit in D by ;
reconsider Uit = Uit as non empty Subset of R^1 by ;
( [#] R^1 <> {} & Uit is open ) by ;
then FnT " Uit is open by ;
then consider SF being Subset-Family of [:(Y | N2),(I[01] | Ti):] such that
A77: FnT " Uit = union SF and
A78: for e being set st e in SF holds
ex X1 being Subset of (Y | N2) ex Y1 being Subset of (I[01] | Ti) st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) by BORSUK_1:5;
A79: TT . i in {(TT . i)} by TARSKI:def 1;
then A80: [y,(TT . i)] in [:N2,{(TT . i)}:] by ;
then FnT . [y,(TT . i)] in Uit by ;
then [y,(TT . i)] in FnT " Uit by ;
then consider N5 being set such that
A81: [y,(TT . i)] in N5 and
A82: N5 in SF by ;
set f = CircleMap | Uit;
A83: dom (CircleMap | Uit) = Uit by ;
A84: rng (CircleMap | Uit) c= Ui
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; :: thesis: b in Ui
then consider a being object such that
A85: a in dom (CircleMap | Uit) and
A86: (CircleMap | Uit) . a = b by FUNCT_1:def 3;
a in union D by ;
then CircleMap . a in Ui by ;
hence b in Ui by ; :: thesis: verum
end;
consider X1 being Subset of (Y | N2), Y1 being Subset of (I[01] | Ti) such that
A87: N5 = [:X1,Y1:] and
A88: X1 is open and
Y1 is open by ;
the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),(() | Ui) by ;
consider NY being Subset of Y such that
A89: NY is open and
A90: NY /\ ([#] (Y | N2)) = X1 by ;
consider y1, y2 being object such that
A91: y1 in X1 and
A92: y2 in Y1 and
A93: [y,(TT . i)] = [y1,y2] by ;
set N1 = NY /\ N2;
y = y1 by ;
then A94: y in NY by ;
then reconsider N1 = NY /\ N2 as non empty open Subset of Y by ;
A95: N1 c= N2 by XBOOLE_1:17;
then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N2,[.(TT . i),(TT . (i + 1)).]:] by ZFMISC_1:96;
then [:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] by A66;
then A96: F .: [:N1,[.(TT . i),(TT . (i + 1)).]:] c= F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by RELAT_1:123;
TT . (i + 1) <= 1 by ;
then reconsider SS = [.(TT . i),(TT . (i + 1)).] as non empty Subset of I[01] by ;
A97: dom (F | [:N1,SS:]) = [:N1,SS:] by ;
set Fni1 = (f ") * (F | [:N1,SS:]);
f " is being_homeomorphism by ;
then A98: dom (f ") = [#] (() | Ui) ;
A99: rng (F | [:N1,SS:]) c= dom (f ")
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (F | [:N1,SS:]) or b in dom (f ") )
assume b in rng (F | [:N1,SS:]) ; :: thesis: b in dom (f ")
then consider a being object such that
A100: a in dom (F | [:N1,SS:]) and
A101: (F | [:N1,SS:]) . a = b by FUNCT_1:def 3;
b = F . a by ;
then b in F .: [:N1,SS:] by ;
then b in F .: [:N,SS:] by A96;
then b in Ui by A48;
hence b in dom (f ") by ; :: thesis: verum
end;
then A102: dom ((f ") * (F | [:N1,SS:])) = dom (F | [:N1,SS:]) by RELAT_1:27;
set Fn2 = Fn | [:N1,S:];
A103: the carrier of (Y | N1) = N1 by PRE_TOPC:8;
then A104: [:N1,S:] = the carrier of [:(Y | N1),():] by ;
then A105: dom (Fn | [:N1,S:]) = the carrier of [:(Y | N1),():] by ;
reconsider ff = f as Function ;
A106: f is being_homeomorphism by ;
then A107: f is one-to-one ;
A108: rng (Fn | [:N1,S:]) c= the carrier of R^1 ;
the carrier of (R^1 | Uit) is Subset of R^1 by TSEP_1:1;
then A109: rng ((f ") * (F | [:N1,SS:])) c= the carrier of R^1 by XBOOLE_1:1;
A110: the carrier of (I[01] | SS) = SS by PRE_TOPC:8;
then A111: [:N1,SS:] = the carrier of [:(Y | N1),(I[01] | SS):] by ;
then reconsider Fni1 = (f ") * (F | [:N1,SS:]) as Function of [:(Y | N1),(I[01] | SS):],R^1 by ;
set Fn1 = (Fn | [:N1,S:]) +* Fni1;
reconsider Fn2 = Fn | [:N1,S:] as Function of [:(Y | N1),():],R^1 by ;
A112: rng ((Fn | [:N1,S:]) +* Fni1) c= (rng (Fn | [:N1,S:])) \/ (rng Fni1) by FUNCT_4:17;
dom (Fn | [:N1,S:]) = [:N1,S:] by ;
then A113: dom ((Fn | [:N1,S:]) +* Fni1) = [:N1,S:] \/ [:N1,SS:] by ;
A114: rng f = [#] (() | Ui) by A106;
then f is onto ;
then A115: f " = ff " by ;
A116: Y1 = Ti
proof
thus Y1 c= Ti by A70; :: according to XBOOLE_0:def 10 :: thesis: Ti c= Y1
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Ti or a in Y1 )
assume a in Ti ; :: thesis: a in Y1
then a = TT . i by TARSKI:def 1;
hence a in Y1 by ; :: thesis: verum
end;
A117: Fn .: [:N1,{(TT . i)}:] c= Uit
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Fn .: [:N1,{(TT . i)}:] or b in Uit )
assume b in Fn .: [:N1,{(TT . i)}:] ; :: thesis: b in Uit
then consider a being Point of [:(Y | N2),():] such that
A118: a in [:N1,{(TT . i)}:] and
A119: Fn . a = b by FUNCT_2:65;
a in N5 by ;
then A120: a in union SF by ;
then a in dom FnT by ;
then Fn . a = FnT . a by FUNCT_1:47;
hence b in Uit by ; :: thesis: verum
end;
A121: for p being set st p in ([#] [:(Y | N1),():]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds
Fn2 . p = Fni1 . p
proof
A122: the carrier of (Y | N2) = N2 by PRE_TOPC:8;
let p be set ; :: thesis: ( p in ([#] [:(Y | N1),():]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p )
assume A123: p in ([#] [:(Y | N1),():]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; :: thesis: Fn2 . p = Fni1 . p
A124: p in ([#] [:(Y | N1),(I[01] | SS):]) /\ ([#] [:(Y | N1),():]) by A123;
then A125: Fn . p = Fn2 . p by ;
[:N1,S:] /\ [:N1,SS:] = [:N1,(S /\ SS):] by ZFMISC_1:99;
then A126: p in [:N1,{(TT . i)}:] by ;
then consider p1 being Element of N1, p2 being Element of {(TT . i)} such that
A127: p = [p1,p2] by DOMAIN_1:1;
A128: p1 in N1 ;
S /\ SS = {(TT . i)} by ;
then p2 in S by XBOOLE_0:def 4;
then A129: p in [:N2,S:] by ;
then A130: Fn . p in Fn .: [:N1,{(TT . i)}:] by ;
(F | [:N1,SS:]) . p = F . p by
.= (F | [:N2,S:]) . p by
.= CircleMap . (Fn . p) by
.= (CircleMap | Uit) . (Fn . p) by
.= ff . (Fn2 . p) by ;
hence Fn2 . p = (ff ") . ((F | [:N1,SS:]) . p) by
.= Fni1 . p by ;
:: thesis: verum
end;
A131: [:N1,S:] c= [:N2,S:] by ;
then reconsider K0 = [:N1,S:] as Subset of [:(Y | N2),():] by ;
A132: [:N1,SS:] c= dom F by ;
reconsider gF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],() by ;
reconsider fF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],(() | Ui) by ;
[:(Y | N1),(I[01] | SS):] = | [:N1,SS:] by BORSUK_3:22;
then gF is continuous by ;
then A133: fF is continuous by TOPMETR:6;
f " is continuous by A106;
then (f ") * fF is continuous by A133;
then A134: Fni1 is continuous by PRE_TOPC:26;
reconsider aN1 = N1 as non empty Subset of (Y | N2) by ;
S c= S ;
then reconsider aS = S as non empty Subset of () by PRE_TOPC:8;
[:(Y | N2),():] | K0 = [:((Y | N2) | aN1),(() | aS):] by BORSUK_3:22
.= [:(Y | N1),(() | aS):] by GOBOARD9:2
.= [:(Y | N1),():] by GOBOARD9:2 ;
then A135: Fn2 is continuous by ;
take N1 ; :: thesis: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N1),():],R^1 st
( S = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )

take S1 = S \/ SS; :: thesis: ex Fn being Function of [:(Y | N1),(I[01] | S1):],R^1 st
( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn is continuous & F | [:N1,S1:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )

A136: [:N1,S:] \/ [:N1,SS:] = [:N1,S1:] by ZFMISC_1:97;
A137: the carrier of (I[01] | S1) = S1 by PRE_TOPC:8;
then [:N1,S1:] = the carrier of [:(Y | N1),(I[01] | S1):] by ;
then reconsider Fn1 = (Fn | [:N1,S:]) +* Fni1 as Function of [:(Y | N1),(I[01] | S1):],R^1 by ;
take Fn1 ; :: thesis: ( S1 = [.0,(TT . (i + 1)).] & y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )
thus A138: S1 = [.0,(TT . (i + 1)).] by ; :: thesis: ( y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )
0 <= TT . (i + 1) by ;
then 0 in S1 by ;
then A139: {0} c= S1 by ZFMISC_1:31;
A140: dom (Fn1 | [: the carrier of Y,:]) = (dom Fn1) /\ [: the carrier of Y,:] by RELAT_1:61;
then A141: dom (Fn1 | [: the carrier of Y,:]) = [:(N1 /\ the carrier of Y),(S1 /\ ):] by
.= [:N1,(S1 /\ ):] by XBOOLE_1:28
.= [:N1,:] by ;
A142: for a being object st a in dom (Fn1 | [: the carrier of Y,:]) holds
(Fn1 | [: the carrier of Y,:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
proof
let a be object ; :: thesis: ( a in dom (Fn1 | [: the carrier of Y,:]) implies (Fn1 | [: the carrier of Y,:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a )
A143: [:N1, the carrier of I[01]:] c= [:N2, the carrier of I[01]:] by ;
assume A144: a in dom (Fn1 | [: the carrier of Y,:]) ; :: thesis: (Fn1 | [: the carrier of Y,:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
then A145: a in [: the carrier of Y,:] by ;
then consider a1, a2 being object such that
a1 in the carrier of Y and
A146: a2 in and
A147: a = [a1,a2] by ZFMISC_1:def 2;
A148: a2 = 0 by ;
0 in S by ;
then {0} c= S by ZFMISC_1:31;
then A149: [:N1,:] c= [:N1,S:] by ZFMISC_1:96;
then A150: a in [:N1,S:] by ;
A151: [:N1,S:] c= [:N1, the carrier of I[01]:] by ZFMISC_1:96;
then A152: a in [:N1, the carrier of I[01]:] by A150;
per cases ( not a in dom Fni1 or a in dom Fni1 ) ;
suppose A153: not a in dom Fni1 ; :: thesis: (Fn1 | [: the carrier of Y,:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
thus (Fn1 | [: the carrier of Y,:]) . a = Fn1 . a by
.= (Fn | [:N1,S:]) . a by
.= Fn . a by
.= (Ft | [:N2, the carrier of I[01]:]) . a by
.= Ft . a by
.= (Ft | [:N1, the carrier of I[01]:]) . a by ; :: thesis: verum
end;
suppose A154: a in dom Fni1 ; :: thesis: (Fn1 | [: the carrier of Y,:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
set e = (Ft | [:N1, the carrier of I[01]:]) . a;
a in [:N1,SS:] by ;
then consider b1, b2 being object such that
A155: b1 in N1 and
A156: b2 in SS and
A157: a = [b1,b2] by ZFMISC_1:def 2;
a2 = b2 by ;
then A158: a2 = TT . i by ;
a1 = b1 by ;
then A159: ( [a1,(TT . i)] in [:N1,S:] & [a1,(TT . i)] in [:N1,{(TT . i)}:] ) by ;
(Ft | [:N1, the carrier of I[01]:]) . a = Ft . a by
.= (Ft | [:N2, the carrier of I[01]:]) . a by
.= Fn . a by ;
then A160: (Ft | [:N1, the carrier of I[01]:]) . a in Fn .: [:N1,{(TT . i)}:] by ;
then A161: ff . ((Ft | [:N1, the carrier of I[01]:]) . a) = CircleMap . ((Ft | [:N1, the carrier of I[01]:]) . a) by
.= CircleMap . (Ft . a) by
.= () . a by
.= F . a by ;
thus (Fn1 | [: the carrier of Y,:]) . a = Fn1 . a by
.= Fni1 . a by
.= (ff ") . ((F | [:N1,SS:]) . a) by
.= (ff ") . (F . a) by
.= (Ft | [:N1, the carrier of I[01]:]) . a by ; :: thesis: verum
end;
end;
end;
A162: rng Fn1 c= dom CircleMap by ;
then A163: dom (CircleMap * Fn1) = dom Fn1 by RELAT_1:27;
A164: for a being object st a in dom (CircleMap * Fn1) holds
(CircleMap * Fn1) . a = F . a
proof
let a be object ; :: thesis: ( a in dom (CircleMap * Fn1) implies (CircleMap * Fn1) . a = F . a )
assume A165: a in dom (CircleMap * Fn1) ; :: thesis: (CircleMap * Fn1) . a = F . a
per cases ( a in dom Fni1 or not a in dom Fni1 ) ;
suppose A166: a in dom Fni1 ; :: thesis: (CircleMap * Fn1) . a = F . a
A167: [:N1,SS:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
A168: a in [:N1,SS:] by ;
then F . a in F .: [:N1,SS:] by ;
then A169: F . a in F .: [:N,SS:] by A96;
then a in F " (dom (ff ")) by ;
then A170: a in dom ((ff ") * F) by RELAT_1:147;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by
.= CircleMap . (Fni1 . a) by
.= CircleMap . ((f ") . ((F | [:N1,SS:]) . a)) by
.= CircleMap . ((f ") . (F . a)) by
.= CircleMap . (((ff ") * F) . a) by
.= (CircleMap * ((ff ") * F)) . a by
.= ((CircleMap * (ff ")) * F) . a by RELAT_1:36
.= (CircleMap * (ff ")) . (F . a) by
.= F . a by ; :: thesis: verum
end;
suppose A171: not a in dom Fni1 ; :: thesis: (CircleMap * Fn1) . a = F . a
then A172: a in [:N1,S:] by ;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by
.= CircleMap . ((Fn | [:N1,S:]) . a) by
.= CircleMap . (Fn . a) by
.= () . a by
.= F . a by ; :: thesis: verum
end;
end;
end;
A173: S c= S1 by XBOOLE_1:7;
then A174: ( [#] (I[01] | S1) = the carrier of (I[01] | S1) & I[01] | S is SubSpace of I[01] | S1 ) by ;
A175: SS c= S1 by XBOOLE_1:7;
then reconsider F1 = [#] (), F2 = [#] (I[01] | SS) as Subset of (I[01] | S1) by ;
reconsider hS = F1, hSS = F2 as Subset of I[01] by PRE_TOPC:8;
hS is closed by ;
then A176: F1 is closed by TSEP_1:8;
thus y in N1 by ; :: thesis: ( N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )
thus N1 c= N by ; :: thesis: ( Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )
hSS is closed by ;
then A177: F2 is closed by TSEP_1:8;
I[01] | SS is SubSpace of I[01] | S1 by ;
then ex h being Function of [:(Y | N1),(I[01] | S1):],R^1 st
( h = Fn2 +* Fni1 & h is continuous ) by ;
hence Fn1 is continuous ; :: thesis: ( F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] )
dom Fn1 = (dom F) /\ [:N1,S1:] by ;
hence F | [:N1,S1:] = CircleMap * Fn1 by ; :: thesis: Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:]
dom (Ft | [:N1, the carrier of I[01]:]) = (dom Ft) /\ [:N1, the carrier of I[01]:] by RELAT_1:61
.= [:( the carrier of Y /\ N1),( /\ the carrier of I[01]):] by
.= [:N1,( /\ the carrier of I[01]):] by XBOOLE_1:28
.= [:N1,:] by ;
hence Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] by ; :: thesis: verum
end;
end;
end;
A178: S2[ 0 ] by FINSEQ_3:24;
for i being Nat holds S2[i] from then consider N2 being non empty open Subset of Y, S being non empty Subset of I[01], Fn1 being Function of [:(Y | N2),():],R^1 such that
A179: S = [.0,(TT . (len TT)).] and
A180: y in N2 and
A181: N2 c= N and
A182: Fn1 is continuous and
A183: F | [:N2,S:] = CircleMap * Fn1 and
A184: Fn1 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] by A17;
Fn1 . x in REAL by XREAL_0:def 1;
then reconsider z = Fn1 . x as Point of R^1 by TOPMETR:17;
A185: I[01] | S = I[01] by ;
then reconsider Fn1 = Fn1 as Function of [:(Y | N2),I[01]:],R^1 ;
take z ; :: thesis: S1[x,z]
take y ; :: thesis: ex t being Point of I[01] ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) )

take t ; :: thesis: ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] & ( for H being Function of [:(Y | N),I[01]:],R^1 st H is continuous & F | [:N, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) )

take N2 ; :: thesis: ex Fn being Function of [:(Y | N2),I[01]:],R^1 st
( x = [y,t] & z = Fn . x & y in N2 & Fn is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] holds
Fn = H ) )

take Fn1 ; :: thesis: ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & ( for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] holds
Fn1 = H ) )

thus ( x = [y,t] & z = Fn1 . x & y in N2 & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] ) by ; :: thesis: for H being Function of [:(Y | N2),I[01]:],R^1 st H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] holds
Fn1 = H

let H be Function of [:(Y | N2),I[01]:],R^1; :: thesis: ( H is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] implies Fn1 = H )
assume that
A186: H is continuous and
A187: F | [:N2, the carrier of I[01]:] = CircleMap * H and
A188: H | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] ; :: thesis: Fn1 = H
defpred S3[ Nat] means ( \$1 in dom TT implies ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . \$1).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] ) );
A189: dom Fn1 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def 1;
A190: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by ;
A191: dom H = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def 1;
A192: for i being Nat st S3[i] holds
S3[i + 1]
proof
let i be Nat; :: thesis: ( S3[i] implies S3[i + 1] )
assume that
A193: S3[i] and
A194: i + 1 in dom TT ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )

per cases ( i = 0 or i in dom TT ) by ;
suppose A195: i = 0 ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )

set Z = [.0,(TT . (i + 1)).];
A196: [.0,(TT . (i + 1)).] = by ;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by ;
A197: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A198: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by ;
A199: for x being object st x in dom (Fn1 | [:N2,Z:]) holds
(Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
proof
let x be object ; :: thesis: ( x in dom (Fn1 | [:N2,Z:]) implies (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x )
A200: [:N2,Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A201: x in dom (Fn1 | [:N2,Z:]) ; :: thesis: (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
hence (Fn1 | [:N2,Z:]) . x = Fn1 . x by
.= (Fn1 | [: the carrier of Y,:]) . x by
.= H . x by
.= (H | [:N2,Z:]) . x by ;
:: thesis: verum
end;
take Z ; :: thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:N2,Z:] = H | [:N2,Z:]
dom (H | [:N2,Z:]) = [:N2,Z:] by ;
hence Fn1 | [:N2,Z:] = H | [:N2,Z:] by ; :: thesis: verum
end;
suppose A202: i in dom TT ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )

set ZZ = [.(TT . i),(TT . (i + 1)).];
A203: 0 <= TT . i by ;
A204: TT . (i + 1) <= 1 by ;
then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by ;
consider Z being non empty Subset of I[01] such that
A205: Z = [.0,(TT . i).] and
A206: Fn1 | [:N2,Z:] = H | [:N2,Z:] by ;
take Z1 = Z \/ ZZ; :: thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] )
A207: TT . i < TT . (i + 1) by ;
hence Z1 = [.0,(TT . (i + 1)).] by ; :: thesis: Fn1 | [:N2,Z1:] = H | [:N2,Z1:]
A208: [:N2,Z1:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A209: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by ;
A210: for x being object st x in dom (Fn1 | [:N2,Z1:]) holds
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
proof
0 <= TT . (i + 1) by ;
then A211: TT . (i + 1) is Point of I[01] by ;
( 0 <= TT . i & TT . i <= 1 ) by ;
then TT . i is Point of I[01] by BORSUK_1:43;
then A212: ZZ is connected by ;
consider Ui being non empty Subset of () such that
A213: Ui in UL and
A214: F .: [:N,ZZ:] c= Ui by ;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A215: union D = CircleMap " Ui and
A216: for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),(() | Ui) st f = CircleMap | d holds
f is being_homeomorphism by ;
let x be object ; :: thesis: ( x in dom (Fn1 | [:N2,Z1:]) implies (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x )
assume A217: x in dom (Fn1 | [:N2,Z1:]) ; :: thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
consider x1, x2 being object such that
A218: x1 in N2 and
A219: x2 in Z1 and
A220: x = [x1,x2] by ;
A221: TT . i in ZZ by ;
then [x1,(TT . i)] in [:N,ZZ:] by ;
then A222: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
reconsider xy = {x1} as non empty Subset of Y by ;
A223: xy c= N2 by ;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by ;
A224: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by ;
A225: D is Cover of Fn1 .: xZZ
proof
let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not b in Fn1 .: xZZ or b in union D )
A226: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; :: thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A227: a in xZZ and
A228: Fn1 . a = b by FUNCT_2:65;
xy c= N by ;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A227;
then A229: F . a in F .: [:N,ZZ:] by ;
CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15
.= F . a by ;
hence b in union D by ; :: thesis: verum
end;
A230: D is Cover of H .: xZZ
proof
let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not b in H .: xZZ or b in union D )
A231: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in H .: xZZ ; :: thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A232: a in xZZ and
A233: H . a = b by FUNCT_2:65;
A234: CircleMap . (H . a) = () . a by FUNCT_2:15
.= F . a by ;
xy c= N by ;
then [:xy,ZZ:] c= [:N,ZZ:] by ZFMISC_1:95;
then a in [:N,ZZ:] by A232;
then F . a in F .: [:N,ZZ:] by ;
hence b in union D by ; :: thesis: verum
end;
A235: H . [x1,(TT . i)] in REAL by XREAL_0:def 1;
TT . i in Z by ;
then A236: [x1,(TT . i)] in [:N2,Z:] by ;
then A237: Fn1 . [x1,(TT . i)] = (Fn1 | [:N2,Z:]) . [x1,(TT . i)] by FUNCT_1:49
.= H . [x1,(TT . i)] by ;
A238: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then F . [x1,(TT . i)] = () . [x1,(TT . i)] by
.= CircleMap . (H . [x1,(TT . i)]) by ;
then H . [x1,(TT . i)] in CircleMap " Ui by ;
then consider Uith being set such that
A239: H . [x1,(TT . i)] in Uith and
A240: Uith in D by ;
A241: Fn1 . [x1,(TT . i)] in REAL by XREAL_0:def 1;
F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by
.= CircleMap . (Fn1 . [x1,(TT . i)]) by ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by ;
then consider Uit being set such that
A242: Fn1 . [x1,(TT . i)] in Uit and
A243: Uit in D by ;
I[01] is SubSpace of I[01] by TSEP_1:2;
then A244: [:(Y | N2),I[01]:] is SubSpace of by BORSUK_3:21;
xy is connected by A218;
then [:xy,ZZ:] is connected by ;
then A245: xZZ is connected by ;
reconsider Uith = Uith as non empty Subset of R^1 by ;
A246: x1 in xy by TARSKI:def 1;
then A247: [x1,(TT . i)] in xZZ by ;
then H . [x1,(TT . i)] in H .: xZZ by FUNCT_2:35;
then Uith meets H .: xZZ by ;
then A248: H .: xZZ c= Uith by ;
reconsider Uit = Uit as non empty Subset of R^1 by ;
set f = CircleMap | Uit;
A249: dom (CircleMap | Uit) = Uit by ;
A250: rng (CircleMap | Uit) c= Ui
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; :: thesis: b in Ui
then consider a being object such that
A251: a in dom (CircleMap | Uit) and
A252: (CircleMap | Uit) . a = b by FUNCT_1:def 3;
a in union D by ;
then CircleMap . a in Ui by ;
hence b in Ui by ; :: thesis: verum
end;
( the carrier of (() | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),(() | Ui) by ;
A253: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by ;
H . [x1,(TT . i)] in H .: xZZ by ;
then Uit meets Uith by ;
then A254: Uit = Uith by ;
A255: rng (H | [:xy,ZZ:]) c= dom f
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (H | [:xy,ZZ:]) or b in dom f )
assume b in rng (H | [:xy,ZZ:]) ; :: thesis: b in dom f
then consider a being object such that
A256: a in dom (H | [:xy,ZZ:]) and
A257: (H | [:xy,ZZ:]) . a = b by FUNCT_1:def 3;
H . a = b by ;
then b in H .: xZZ by ;
hence b in dom f by ; :: thesis: verum
end;
Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by ;
then Uit meets Fn1 .: xZZ by ;
then A258: Fn1 .: xZZ c= Uit by ;
A259: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn1 | [:xy,ZZ:]) ; :: thesis: b in dom f
then consider a being object such that
A260: a in dom (Fn1 | [:xy,ZZ:]) and
A261: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def 3;
Fn1 . a = b by ;
then b in Fn1 .: xZZ by ;
hence b in dom f by ; :: thesis: verum
end;
then A262: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
A263: for x being object st x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
proof
let x be object ; :: thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x )
assume A264: x in dom (f * (Fn1 | [:xy,ZZ:])) ; :: thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
A265: Fn1 . x in Fn1 .: [:xy,ZZ:] by ;
A266: H . x in H .: [:xy,ZZ:] by ;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by
.= f . (Fn1 . x) by
.= CircleMap . (Fn1 . x) by
.= (CircleMap * Fn1) . x by
.= CircleMap . (H . x) by
.= f . (H . x) by
.= (f * H) . x by
.= ((f * H) | [:xy,ZZ:]) . x by
.= (f * (H | [:xy,ZZ:])) . x by RELAT_1:83 ; :: thesis: verum
end;
f is being_homeomorphism by ;
then A267: f is one-to-one ;
dom (f * (H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by ;
then A268: f * (Fn1 | [:xy,ZZ:]) = f * (H | [:xy,ZZ:]) by ;
per cases ( x2 in ZZ or not x2 in ZZ ) ;
suppose x2 in ZZ ; :: thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
then A269: x in [:xy,ZZ:] by ;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by
.= (Fn1 | [:xy,ZZ:]) . x by
.= (H | [:xy,ZZ:]) . x by
.= H . x by
.= (H | [:N2,Z1:]) . x by ; :: thesis: verum
end;
suppose not x2 in ZZ ; :: thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
then x2 in Z by ;
then A270: x in [:N2,Z:] by ;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by
.= (Fn1 | [:N2,Z:]) . x by
.= H . x by
.= (H | [:N2,Z1:]) . x by ; :: thesis: verum
end;
end;
end;
dom (H | [:N2,Z1:]) = [:N2,Z1:] by ;
hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by ; :: thesis: verum
end;
end;
end;
A271: S3[ 0 ] by FINSEQ_3:24;
for i being Nat holds S3[i] from then consider Z being non empty Subset of I[01] such that
A272: Z = [.0,(TT . (len TT)).] and
A273: Fn1 | [:N2,Z:] = H | [:N2,Z:] by A17;
thus Fn1 = Fn1 | [:N2,Z:] by
.= H by ; :: thesis: verum
end;
consider G being Function of ,R^1 such that
A274: for x being Point of holds S1[x,G . x] from take G ; :: thesis: ( G is continuous & F = CircleMap * G & G | [: the carrier of Y,:] = Ft & ( for H being Function of ,R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,:] = Ft holds
G = H ) )

A275: now :: thesis: for N being Subset of Y
for F being Function of [:(Y | N),I[01]:],R^1 holds dom F = [:N, the carrier of I[01]:]
let N be Subset of Y; :: thesis: for F being Function of [:(Y | N),I[01]:],R^1 holds dom F = [:N, the carrier of I[01]:]
let F be Function of [:(Y | N),I[01]:],R^1; :: thesis: dom F = [:N, the carrier of I[01]:]
thus dom F = the carrier of [:(Y | N),I[01]:] by FUNCT_2:def 1
.= [: the carrier of (Y | N), the carrier of I[01]:] by BORSUK_1:def 2
.= [:N, the carrier of I[01]:] by PRE_TOPC:8 ; :: thesis: verum
end;
A276: for p being Point of
for y being Point of Y
for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
proof
let p be Point of ; :: thesis: for y being Point of Y
for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

let y be Point of Y; :: thesis: for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

let t be Point of I[01]; :: thesis: for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

let N1, N2 be non empty open Subset of Y; :: thesis: for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

let Fn1 be Function of [:(Y | N1),I[01]:],R^1; :: thesis: for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

let Fn2 be Function of [:(Y | N2),I[01]:],R^1; :: thesis: ( p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] implies Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] )
assume that
p = [y,t] and
A277: y in N1 and
A278: y in N2 and
A279: Fn2 is continuous and
A280: Fn1 is continuous and
A281: F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 and
A282: Fn2 | [: the carrier of Y,:] = Ft | [:N2, the carrier of I[01]:] and
A283: F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 and
A284: Fn1 | [: the carrier of Y,:] = Ft | [:N1, the carrier of I[01]:] ; :: thesis: Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
A285: {y} c= N1 by ;
consider TT being non empty FinSequence of REAL such that
A286: TT . 1 = 0 and
A287: TT . (len TT) = 1 and
A288: TT is increasing and
A289: ex N being open Subset of Y st
( y in N & ( for i being Nat st i in dom TT & i + 1 in dom TT holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) ) ) by A3, A1, Th21;
consider N being open Subset of Y such that
A290: y in N and
A291: for i being Nat st i in dom TT & i + 1 in dom TT holds
ex Ui being non empty Subset of () st
( Ui in UL & F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui ) by A289;
reconsider N = N as non empty open Subset of Y by A290;
defpred S2[ Nat] means ( \$1 in dom TT implies ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . \$1).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) );
A292: len TT in dom TT by FINSEQ_5:6;
A293: dom Fn2 = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def 1;
A294: dom Fn2 = [:N2, the carrier of I[01]:] by A275;
A295: {y} c= N2 by ;
A296: ( the carrier of [:(Y | N1),I[01]:] = [: the carrier of (Y | N1), the carrier of I[01]:] & the carrier of (Y | N1) = N1 ) by ;
A297: ( the carrier of [:(Y | N2),I[01]:] = [: the carrier of (Y | N2), the carrier of I[01]:] & the carrier of (Y | N2) = N2 ) by ;
A298: dom Fn1 = [:N1, the carrier of I[01]:] by A275;
A299: dom Fn1 = the carrier of [:(Y | N1),I[01]:] by FUNCT_2:def 1;
A300: 1 in dom TT by FINSEQ_5:6;
A301: for i being Nat st S2[i] holds
S2[i + 1]
proof
let i be Nat; :: thesis: ( S2[i] implies S2[i + 1] )
assume that
A302: S2[i] and
A303: i + 1 in dom TT ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )

per cases ( i = 0 or i in dom TT ) by ;
suppose A304: i = 0 ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )

set Z = [.0,(TT . (i + 1)).];
A305: [.0,(TT . (i + 1)).] = by ;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by ;
A306: [:{y},Z:] c= [:N2, the carrier of I[01]:] by ;
A307: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by ;
A308: [:{y},Z:] c= [:N1, the carrier of I[01]:] by ;
A309: for x being object st x in dom (Fn1 | [:{y},Z:]) holds
(Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
proof
let x be object ; :: thesis: ( x in dom (Fn1 | [:{y},Z:]) implies (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x )
A310: [:{y},Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A311: x in dom (Fn1 | [:{y},Z:]) ; :: thesis: (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
hence (Fn1 | [:{y},Z:]) . x = Fn1 . x by
.= (Fn1 | [: the carrier of Y,:]) . x by
.= Ft . x by
.= (Ft | [:N2, the carrier of I[01]:]) . x by
.= Fn2 . x by
.= (Fn2 | [:{y},Z:]) . x by ;
:: thesis: verum
end;
take Z ; :: thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]
dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by ;
hence Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by ; :: thesis: verum
end;
suppose A312: i in dom TT ; :: thesis: ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )

A313: now :: thesis: for i being Element of NAT st i in dom TT holds
( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
let i be Element of NAT ; :: thesis: ( i in dom TT implies ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) ) )
assume A314: i in dom TT ; :: thesis: ( 0 <= TT . i & ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) ) )
1 <= i by ;
then ( 1 = i or 1 < i ) by XXREAL_0:1;
hence A315: 0 <= TT . i by ; :: thesis: ( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) )
assume A316: i + 1 in dom TT ; :: thesis: ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
A317: i + 0 < i + 1 by XREAL_1:8;
hence A318: TT . i < TT . (i + 1) by ; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
i + 1 <= len TT by ;
then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1;
hence TT . (i + 1) <= 1 by ; :: thesis: ( TT . i < 1 & 0 < TT . (i + 1) )
hence TT . i < 1 by ; :: thesis: 0 < TT . (i + 1)
thus 0 < TT . (i + 1) by ; :: thesis: verum
end;
then A319: 0 <= TT . i by A312;
A320: TT . (i + 1) <= 1 by ;
set ZZ = [.(TT . i),(TT . (i + 1)).];
consider Z being non empty Subset of I[01] such that
A321: Z = [.0,(TT . i).] and
A322: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by ;
now :: thesis: for i being Nat st 0 <= TT . i & TT . (i + 1) <= 1 holds
[.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
let i be Nat; :: thesis: ( 0 <= TT . i & TT . (i + 1) <= 1 implies [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] )
assume that
A323: 0 <= TT . i and
A324: TT . (i + 1) <= 1 ; :: thesis: [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] :: thesis: verum
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in [.(TT . i),(TT . (i + 1)).] or a in the carrier of I[01] )
assume A325: a in [.(TT . i),(TT . (i + 1)).] ; :: thesis: a in the carrier of I[01]
then reconsider a = a as Real ;
a <= TT . (i + 1) by ;
then A326: a <= 1 by ;
0 <= a by ;
hence a in the carrier of I[01] by ; :: thesis: verum
end;
end;
then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by ;
take Z1 = Z \/ ZZ; :: thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] )
A327: TT . i < TT . (i + 1) by ;
hence Z1 = [.0,(TT . (i + 1)).] by ; :: thesis: Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]
A328: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by ;
A329: for x being object st x in dom (Fn1 | [:{y},Z1:]) holds
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
proof
0 <= TT . (i + 1) by ;
then A330: TT . (i + 1) is Point of I[01] by ;
( 0 <= TT . i & TT . i <= 1 ) by ;
then TT . i is Point of I[01] by BORSUK_1:43;
then A331: ZZ is connected by ;
A332: TT . i in ZZ by ;
consider Ui being non empty Subset of () such that
A333: Ui in UL and
A334: F .: [:N,ZZ:] c= Ui by ;
consider D being mutually-disjoint open Subset-Family of R^1 such that
A335: union D = CircleMap " Ui and
A336: for d being Subset of R^1 st d in D holds
for f being Function of (R^1 | d),(() | Ui) st f = CircleMap | d holds
f is being_homeomorphism by ;
let x be object ; :: thesis: ( x in dom (Fn1 | [:{y},Z1:]) implies (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x )
assume A337: x in dom (Fn1 | [:{y},Z1:]) ; :: thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
consider x1, x2 being object such that
A338: x1 in {y} and
A339: x2 in Z1 and
A340: x = [x1,x2] by ;
reconsider xy = {x1} as non empty Subset of Y by ;
A341: xy c= N2 by ;
then A342: [:xy,ZZ:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:96;
A343: x1 = y by ;
then [x1,(TT . i)] in [:N,ZZ:] by ;
then A344: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
A345: xy c= N1 by ;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N1),I[01]:] by ;
xy is connected by A338;
then A346: [:xy,ZZ:] is connected by ;
A347: xy c= N by ;
A348: D is Cover of Fn1 .: xZZ
proof
let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not b in Fn1 .: xZZ or b in union D )
A349: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; :: thesis: b in union D
then consider a being Point of [:(Y | N1),I[01]:] such that
A350: a in xZZ and
A351: Fn1 . a = b by FUNCT_2:65;
A352: CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15
.= F . a by ;
[:xy,ZZ:] c= [:N,ZZ:] by ;
then a in [:N,ZZ:] by A350;
then F . a in F .: [:N,ZZ:] by ;
hence b in union D by ; :: thesis: verum
end;
A353: I[01] is SubSpace of I[01] by TSEP_1:2;
then [:(Y | N1),I[01]:] is SubSpace of by BORSUK_3:21;
then A354: xZZ is connected by ;
reconsider XZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by ;
[:(Y | N2),I[01]:] is SubSpace of by ;
then A355: XZZ is connected by ;
A356: D is Cover of Fn2 .: xZZ
proof
let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis: ( not b in Fn2 .: xZZ or b in union D )
A357: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn2 .: xZZ ; :: thesis: b in union D
then consider a being Point of [:(Y | N2),I[01]:] such that
A358: a in xZZ and
A359: Fn2 . a = b by FUNCT_2:65;
A360: CircleMap . (Fn2 . a) = (CircleMap * Fn2) . a by FUNCT_2:15
.= F . a by ;
[:xy,ZZ:] c= [:N,ZZ:] by ;
then a in [:N,ZZ:] by A358;
then F . a in F .: [:N,ZZ:] by ;
hence b in union D by ; :: thesis: verum
end;
A361: TT . i in Z by ;
then A362: [x1,(TT . i)] in [:{y},Z:] by ;
A363: Fn1 . [x1,(TT . i)] in REAL by XREAL_0:def 1;
A364: [:{y},Z:] c= [:N1, the carrier of I[01]:] by ;
then F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by
.= CircleMap . (Fn1 . [x1,(TT . i)]) by ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by ;
then consider Uit being set such that
A365: Fn1 . [x1,(TT . i)] in Uit and
A366: Uit in D by ;
reconsider Uit = Uit as non empty Subset of R^1 by ;
set f = CircleMap | Uit;
A367: dom (CircleMap | Uit) = Uit by ;
A368: rng (CircleMap | Uit) c= Ui
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (CircleMap | Uit) or b in Ui )
assume b in rng (CircleMap | Uit) ; :: thesis: b in Ui
then consider a being object such that
A369: a in dom (CircleMap | Uit) and
A370: (CircleMap | Uit) . a = b by FUNCT_1:def 3;
a in union D by ;
then CircleMap . a in Ui by ;
hence b in Ui by ; :: thesis: verum
end;
( the carrier of (() | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),(() | Ui) by ;
A371: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
A372: Fn2 . [x1,(TT . i)] in REAL by XREAL_0:def 1;
A373: [x1,(TT . i)] in [:N2,Z:] by ;
then F . [x1,(TT . i)] = (CircleMap * Fn2) . [x1,(TT . i)] by
.= CircleMap . (Fn2 . [x1,(TT . i)]) by ;
then Fn2 . [x1,(TT . i)] in CircleMap " Ui by ;
then consider Uith being set such that
A374: Fn2 . [x1,(TT . i)] in Uith and
A375: Uith in D by ;
reconsider Uith = Uith as non empty Subset of R^1 by ;
A376: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by ;
A377: x1 in xy by TARSKI:def 1;
then A378: [x1,(TT . i)] in xZZ by ;
then Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by FUNCT_2:35;
then Uit meets Fn1 .: xZZ by ;
then A379: Fn1 .: xZZ c= Uit by ;
A380: rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn1 | [:xy,ZZ:]) ; :: thesis: b in dom f
then consider a being object such that
A381: a in dom (Fn1 | [:xy,ZZ:]) and
A382: (Fn1 | [:xy,ZZ:]) . a = b by FUNCT_1:def 3;
Fn1 . a = b by ;
then b in Fn1 .: xZZ by ;
hence b in dom f by ; :: thesis: verum
end;
then A383: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
[x1,(TT . i)] in [:xy,ZZ:] by ;
then [x1,(TT . i)] in dom Fn2 by ;
then A384: Fn2 . [x1,(TT . i)] in Fn2 .: xZZ by ;
then Uith meets Fn2 .: xZZ by ;
then A385: Fn2 .: xZZ c= Uith by ;
Fn1 . [x1,(TT . i)] = (Fn1 | [:{y},Z:]) . [x1,(TT . i)] by
.= Fn2 . [x1,(TT . i)] by ;
then Uit meets Uith by ;
then A386: Uit = Uith by ;
A387: for x being object st x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
proof
A388: dom (Fn1 | [:xy,ZZ:]) c= dom Fn1 by RELAT_1:60;
let x be object ; :: thesis: ( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x )
assume A389: x in dom (f * (Fn1 | [:xy,ZZ:])) ; :: thesis: (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
A390: Fn1 . x in Fn1 .: [:xy,ZZ:] by ;
A391: Fn2 . x in Fn2 .: [:xy,ZZ:] by ;
dom (Fn1 | [:xy,ZZ:]) = (dom Fn1) /\ [:xy,ZZ:] by RELAT_1:61;
then A392: x in [:xy,ZZ:] by ;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by
.= f . (Fn1 . x) by
.= CircleMap . (Fn1 . x) by
.= (CircleMap * Fn1) . x by
.= F . x by
.= (CircleMap * Fn2) . x by
.= CircleMap . (Fn2 . x) by
.= f . (Fn2 . x) by
.= (f * Fn2) . x by
.= ((f * Fn2) | [:xy,ZZ:]) . x by
.= (f * (Fn2 | [:xy,ZZ:])) . x by RELAT_1:83 ; :: thesis: verum
end;
A393: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by ;
A394: rng (Fn2 | [:xy,ZZ:]) c= dom f
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng (Fn2 | [:xy,ZZ:]) or b in dom f )
assume b in rng (Fn2 | [:xy,ZZ:]) ; :: thesis: b in dom f
then consider a being object such that
A395: a in dom (Fn2 | [:xy,ZZ:]) and
A396: (Fn2 | [:xy,ZZ:]) . a = b by FUNCT_1:def 3;
Fn2 . a = b by ;
then b in Fn2 .: xZZ by ;
hence b in dom f by ; :: thesis: verum
end;
then dom (f * (Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:]) by RELAT_1:27;
then A397: f * (Fn1 | [:xy,ZZ:]) = f * (Fn2 | [:xy,ZZ:]) by ;
f is being_homeomorphism by ;
then A398: f is one-to-one ;
per cases ( x2 in ZZ or not x2 in ZZ ) ;
suppose x2 in ZZ ; :: thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
then A399: x in [:xy,ZZ:] by ;
thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by
.= (Fn1 | [:xy,ZZ:]) . x by
.= (Fn2 | [:xy,ZZ:]) . x by
.= Fn2 . x by
.= (Fn2 | [:{y},Z1:]) . x by ; :: thesis: verum
end;
suppose not x2 in ZZ ; :: thesis: (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) .<