consider UL being Subset-Family of (Tunit_circle 2) such that
A1: ( UL is Cover of (Tunit_circle 2) & UL is open ) and
A2: for U being Subset of (Tunit_circle 2) 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),((Tunit_circle 2) | U) st f = CircleMap | d holds
f is being_homeomorphism ) ) by Lm13;
let Y be non empty TopSpace; :: thesis:
let F be Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis:
let Ft be Function of [:Y,(Sspace 0[01]):],R^1; :: thesis:
assume that
A3: F is continuous and
A4: Ft is continuous and
A5: F | [: the carrier of Y,{0}:] = CircleMap * Ft ; :: thesis:
defpred S₁[ 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,{0}:] = 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,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H ) );
A6: dom F = the carrier of [:Y,I[01]:] by FUNCT_2:def 1
.= [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2 ;
A7: the carrier of [:Y,(Sspace 0[01]):] = [: the carrier of Y, the carrier of (Sspace 0[01]):] by BORSUK_1:def 2;
then A8: dom Ft = [: the carrier of Y,{0}:] by Lm14, FUNCT_2:def 1;
A9: for x being Point of [:Y,I[01]:] ex z being Point of R^1 st S₁[x,z]

proof

let x be Point of [:Y,I[01]:]; :: thesis:
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 (Tunit_circle 2) 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 (Tunit_circle 2) 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 S₂[ 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),(I[01] | S):],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,{0}:] = 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:

let i be Element of NAT ; :: thesis:
assume A20: i in dom TT ; :: thesis:
1 <= i by A20, FINSEQ_3:25;
then ( 1 = i or 1 < i ) by XXREAL_0:1;
hence A21: 0 <= TT . i by A11, A13, A18, A20, SEQM_3:def 1; :: thesis:
assume A22: i + 1 in dom TT ; :: thesis:
A23: i + 0 < i + 1 by XREAL_1:8;
hence A24: TT . i < TT . (i + 1) by A13, A20, A22, SEQM_3:def 1; :: thesis:
i + 1 <= len TT by A22, FINSEQ_3:25;
then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1;
hence TT . (i + 1) <= 1 by A12, A13, A17, A22, SEQM_3:def 1; :: thesis:
hence TT . i < 1 by A24, XXREAL_0:2; :: thesis:
thus 0 < TT . (i + 1) by A13, A20, A21, A22, A23, SEQM_3:def 1; :: thesis:

end;

A25: now :: thesis:

let i be Nat; :: thesis:
assume that
A26: 0 <= TT . i and
A27: TT . (i + 1) <= 1 ; :: thesis:
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A28: a in [.(TT . i),(TT . (i + 1)).] ; :: thesis:
then reconsider a = a as Real ;
a <= TT . (i + 1) by A28, XXREAL_1:1;
then A29: a <= 1 by A27, XXREAL_0:2;
0 <= a by A26, A28, XXREAL_1:1;
hence a in the carrier of I[01] by A29, BORSUK_1:43; :: thesis:

end;

A30: for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume that
A31: S₂[i] and
A32: i + 1 in dom TT ; :: thesis:

per cases by A32, TOPREALA:2;

suppose A33: i = 0 ; :: thesis:

take N2 = N; :: thesis:
set Fn = Ft | [:N2,{0}:];
set S = [.0,(TT . (i + 1)).];
A34: [.0,(TT . (i + 1)).] = {0} by A11, A33, XXREAL_1:17;
reconsider S = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A33, Lm3, XXREAL_1:17;
A35: dom (Ft | [:N2,{0}:]) = [:N2,S:] by A8, A34, RELAT_1:62, ZFMISC_1:96;
reconsider K0 = [:N2,S:] as non empty Subset of [:Y,(Sspace 0[01]):] by A7, A34, Lm14, ZFMISC_1:96;
A36: ( the carrier of [:(Y | N2),(I[01] | S):] = [: the carrier of (Y | N2), the carrier of (I[01] | S):] & rng (Ft | [:N2,{0}:]) c= the carrier of R^1 ) by BORSUK_1:def 2, RELAT_1:def 19;
( the carrier of (Y | N2) = N2 & the carrier of (I[01] | S) = S ) by PRE_TOPC:8;
then reconsider Fn = Ft | [:N2,{0}:] as Function of [:(Y | N2),(I[01] | S):],R^1 by A35, A36, FUNCT_2:2;
A37: dom (F | [:N2,S:]) = [:N2,S:] by A6, RELAT_1:62, ZFMISC_1:96;
reconsider S1 = S as non empty Subset of (Sspace 0[01]) by A11, A33, Lm14, XXREAL_1:17;
take S ; :: thesis:
take Fn ; :: thesis:
thus S = [.0,(TT . (i + 1)).] ; :: thesis:
thus y in N2 by A15; :: thesis:
thus N2 c= N ; :: thesis:
I[01] | S = Sspace 0[01] by A34, TOPALG_3:5
.= (Sspace 0[01]) | S1 by A34, Lm14, TSEP_1:3 ;
then [:(Y | N2),(I[01] | S):] = [:Y,(Sspace 0[01]):] | K0 by BORSUK_3:22;
hence Fn is continuous by A4, A34, TOPMETR:7; :: thesis:
rng Fn c= dom CircleMap by Lm12, TOPMETR:17;
then A38: dom (CircleMap * Fn) = dom Fn by RELAT_1:27;
A39: [:N2,S:] c= dom Ft by A8, A34, ZFMISC_1:96;
for x being object st x in dom (F | [:N2,S:]) holds
(F | [:N2,S:]) . x = (CircleMap * Fn) . x

proof

let x be object ; :: thesis:
assume A40: x in dom (F | [:N2,S:]) ; :: thesis:
thus (F | [:N2,S:]) . x = F . x by A37, A40, FUNCT_1:49
.= (CircleMap * Ft) . x by A5, A7, A35, A37, A40, Lm14, FUNCT_1:49
.= CircleMap . (Ft . x) by A39, A37, A40, FUNCT_1:13
.= CircleMap . (Fn . x) by A34, A37, A40, FUNCT_1:49
.= (CircleMap * Fn) . x by A35, A37, A40, FUNCT_1:13 ; :: thesis:

end;

hence F | [:N2,S:] = CircleMap * Fn by A35, A37, A38; :: thesis:
A41: dom (Fn | [: the carrier of Y,{0}:]) = [:N2,S:] /\ [: the carrier of Y,{0}:] by A35, RELAT_1:61;
A42: for x being object st x in dom (Fn | [: the carrier of Y,{0}:]) holds
(Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x

proof

A43: [:N2,{0}:] c= [:N2, the carrier of I[01]:] by Lm3, ZFMISC_1:95;
let x be object ; :: thesis:
assume A44: x in dom (Fn | [: the carrier of Y,{0}:]) ; :: thesis:
A45: x in [:N2,{0}:] by A34, A41, A44, XBOOLE_0:def 4;
x in [: the carrier of Y,{0}:] by A41, A44, XBOOLE_0:def 4;
hence (Fn | [: the carrier of Y,{0}:]) . x = Fn . x by FUNCT_1:49
.= Ft . x by A45, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . x by A45, A43, FUNCT_1:49 ;
:: thesis:

end;

dom (Ft | [:N2, the carrier of I[01]:]) = [: the carrier of Y,{0}:] /\ [:N2, the carrier of I[01]:] by A8, RELAT_1:61
.= [:N2,S:] by A34, ZFMISC_1:101 ;
hence Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] by A34, A41, A42, ZFMISC_1:101; :: thesis:

end;

suppose A46: i in dom TT ; :: thesis:

set SS = [.(TT . i),(TT . (i + 1)).];
consider Ui being non empty Subset of (Tunit_circle 2) such that
A47: Ui in UL and
A48: F .: [:N,[.(TT . i),(TT . (i + 1)).]:] c= Ui by A16, A32, A46;
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),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A47;
A51: the carrier of ((Tunit_circle 2) | Ui) = Ui by PRE_TOPC:8;
A52: TT . i < TT . (i + 1) by A19, A32, A46;
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 A15, ZFMISC_1:87;
consider N2 being open Subset of Y, S being non empty Subset of I[01], Fn being Function of [:(Y | N2),(I[01] | S):],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,{0}:] = Ft | [:N2, the carrier of I[01]:] by A31, A46;
reconsider N2 = N2 as non empty open Subset of Y by A55;
A60: the carrier of [:(Y | N2),(I[01] | S):] = [: the carrier of (Y | N2), the carrier of (I[01] | S):] 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),(I[01] | S):] by FUNCT_2:def 1;
A62: 0 <= TT . i by A19, A46;
then A63: TT . i in S by A54, XXREAL_1:1;
then reconsider Ti = {(TT . i)} as non empty Subset of I[01] by ZFMISC_1:31;
A64: the carrier of (I[01] | S) = S by PRE_TOPC:8;
then reconsider Ti2 = Ti as non empty Subset of (I[01] | S) by A63, ZFMISC_1:31;
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 BORSUK_1:def 2;
A66: [:N2,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:] by A56, ZFMISC_1:96;
A67: the carrier of (Y | N2) = N2 by PRE_TOPC:8;
{(TT . i)} c= S by A63, ZFMISC_1:31;
then A68: dom (Fn | [:N2,Ti:]) = [:N2,{(TT . i)}:] by A64, A60, A67, A61, RELAT_1:62, ZFMISC_1:96;
A69: [:((Y | N2) | N7),((I[01] | S) | Ti2):] = [:(Y | N2),(I[01] | S):] | [:N7,Ti2:] by BORSUK_3:22;
A70: the carrier of (I[01] | Ti) = Ti by PRE_TOPC:8;
rng (Fn | [:N2,Ti:]) c= the carrier of R^1 by RELAT_1:def 19;
then reconsider FnT = Fn | [:N2,Ti:] as Function of [:(Y | N2),(I[01] | Ti):],R^1 by A67, A68, A65, A70, FUNCT_2:2;
( (Y | N2) | N7 = Y | N2 & (I[01] | S) | Ti2 = I[01] | Ti ) by GOBOARD9:2;
then A71: FnT is continuous by A57, A69, TOPMETR:7;
A72: Fn . [y,(TT . i)] in REAL by XREAL_0:def 1;
[y,(TT . i)] in dom F by A6, A63, ZFMISC_1:87;
then A73: F . [y,(TT . i)] in F .: [:N,[.(TT . i),(TT . (i + 1)).]:] by A53, FUNCT_2:35;
A74: [y,(TT . i)] in [:N2,S:] by A55, A63, ZFMISC_1:87;
then F . [y,(TT . i)] = (CircleMap * Fn) . [y,(TT . i)] by A58, FUNCT_1:49
.= CircleMap . (Fn . [y,(TT . i)]) by A64, A60, A67, A74, FUNCT_2:15 ;
then Fn . [y,(TT . i)] in CircleMap " Ui by A48, A73, FUNCT_2:38, TOPMETR:17, A72;
then consider Uit being set such that
A75: Fn . [y,(TT . i)] in Uit and
A76: Uit in D by A49, TARSKI:def 4;
reconsider Uit = Uit as non empty Subset of R^1 by A75, A76;
( [#] R^1 <> {} & Uit is open ) by A76, TOPS_2:def 1;
then FnT " Uit is open by A71, TOPS_2:43;
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 A55, ZFMISC_1:def 2;
then FnT . [y,(TT . i)] in Uit by A75, FUNCT_1:49;
then [y,(TT . i)] in FnT " Uit by A80, A68, FUNCT_1:def 7;
then consider N5 being set such that
A81: [y,(TT . i)] in N5 and
A82: N5 in SF by A77, TARSKI:def 4;
set f = CircleMap | Uit;
A83: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A84: rng (CircleMap | Uit) c= Ui

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (CircleMap | Uit) ; :: thesis:
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 A76, A83, A85, TARSKI:def 4;
then CircleMap . a in Ui by A49, FUNCT_2:38;
hence b in Ui by A83, A85, A86, FUNCT_1:49; :: thesis:

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 A78, A82;
the carrier of (R^1 | Uit) = Uit by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A51, A83, A84, FUNCT_2:2;
consider NY being Subset of Y such that
A89: NY is open and
A90: NY /\ ([#] (Y | N2)) = X1 by A88, TOPS_2:24;
consider y1, y2 being object such that
A91: y1 in X1 and
A92: y2 in Y1 and
A93: [y,(TT . i)] = [y1,y2] by A81, A87, ZFMISC_1:def 2;
set N1 = NY /\ N2;
y = y1 by A93, XTUPLE_0:1;
then A94: y in NY by A90, A91, XBOOLE_0:def 4;
then reconsider N1 = NY /\ N2 as non empty open Subset of Y by A55, A89, XBOOLE_0:def 4;
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 A19, A32, A46;
then reconsider SS = [.(TT . i),(TT . (i + 1)).] as non empty Subset of I[01] by A25, A62, A52, XXREAL_1:1;
A97: dom (F | [:N1,SS:]) = [:N1,SS:] by A6, RELAT_1:62, ZFMISC_1:96;
set Fni1 = (f ") * (F | [:N1,SS:]);
f " is being_homeomorphism by A50, A76, TOPS_2:56;
then A98: dom (f ") = [#] ((Tunit_circle 2) | Ui) ;
A99: rng (F | [:N1,SS:]) c= dom (f ")

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (F | [:N1,SS:]) ; :: thesis:
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 A97, A100, A101, FUNCT_1:49;
then b in F .: [:N1,SS:] by A97, A100, FUNCT_2:35;
then b in F .: [:N,SS:] by A96;
then b in Ui by A48;
hence b in dom (f ") by A98, PRE_TOPC:8; :: thesis:

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),(I[01] | S):] by A64, BORSUK_1:def 2;
then A105: dom (Fn | [:N1,S:]) = the carrier of [:(Y | N1),(I[01] | S):] by A64, A60, A67, A61, A95, RELAT_1:62, ZFMISC_1:96;
reconsider ff = f as Function ;
A106: f is being_homeomorphism by A50, A76;
then A107: f is one-to-one ;
A108: rng (Fn | [:N1,S:]) c= the carrier of R^1 by RELAT_1:def 19;
AAA: rng ((f ") * (F | [:N1,SS:])) c= the carrier of (R^1 | Uit) by RELAT_1:def 19;
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 AAA, 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 A103, BORSUK_1:def 2;
then reconsider Fni1 = (f ") * (F | [:N1,SS:]) as Function of [:(Y | N1),(I[01] | SS):],R^1 by A97, A102, A109, FUNCT_2:2;
reconsider Fn2 = Fn | [:N1,S:] as Function of [:(Y | N1),(I[01] | S):],R^1 by A105, A108, FUNCT_2:2;
set Fn1 = Fn2 +* Fni1;
A112: rng (Fn2 +* Fni1) c= (rng Fn2) \/ (rng Fni1) by FUNCT_4:17;
dom (Fn | [:N1,S:]) = [:N1,S:] by A64, A60, A67, A61, A95, RELAT_1:62, ZFMISC_1:96;
then A113: dom (Fn2 +* Fni1) = [:N1,S:] \/ [:N1,SS:] by A97, A102, FUNCT_4:def 1;
A114: rng f = [#] ((Tunit_circle 2) | Ui) by A106;
then f is onto ;
then A115: f " = ff " by A107, TOPS_2:def 4;
A116: Y1 = Ti

proof

thus Y1 c= Ti by A70; :: according to XBOOLE_0:def 10 :: thesis:
let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in Ti ; :: thesis:
then a = TT . i by TARSKI:def 1;
hence a in Y1 by A92, A93, XTUPLE_0:1; :: thesis:

end;

A117: Fn .: [:N1,{(TT . i)}:] c= Uit

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in Fn .: [:N1,{(TT . i)}:] ; :: thesis:
then consider a being Point of [:(Y | N2),(I[01] | S):] such that
A118: a in [:N1,{(TT . i)}:] and
A119: Fn . a = b by FUNCT_2:65;
a in N5 by A87, A90, A116, A118, PRE_TOPC:def 5;
then A120: a in union SF by A82, TARSKI:def 4;
then a in dom FnT by A77, FUNCT_1:def 7;
then Fn . a = FnT . a by FUNCT_1:47;
hence b in Uit by A77, A119, A120, FUNCT_1:def 7; :: thesis:

end;

A121: for p being set st p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(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:
assume A123: p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; :: thesis:
A124: p in ([#] [:(Y | N1),(I[01] | SS):]) /\ ([#] [:(Y | N1),(I[01] | S):]) by A123;
then A125: Fn . p = Fn2 . p by A104, FUNCT_1:49;
[:N1,S:] /\ [:N1,SS:] = [:N1,(S /\ SS):] by ZFMISC_1:99;
then A126: p in [:N1,{(TT . i)}:] by A54, A62, A52, A111, A104, A123, XXREAL_1:418;
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 A54, A62, A52, XXREAL_1:418;
then p2 in S by XBOOLE_0:def 4;
then A129: p in [:N2,S:] by A95, A127, A128, ZFMISC_1:def 2;
then A130: Fn . p in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A126, FUNCT_2:35;
(F | [:N1,SS:]) . p = F . p by A111, A123, FUNCT_1:49
.= (F | [:N2,S:]) . p by A129, FUNCT_1:49
.= CircleMap . (Fn . p) by A58, A64, A60, A61, A122, A129, FUNCT_1:13
.= (CircleMap | Uit) . (Fn . p) by A117, A130, FUNCT_1:49
.= ff . (Fn2 . p) by A104, A124, FUNCT_1:49 ;
hence Fn2 . p = (ff ") . ((F | [:N1,SS:]) . p) by A117, A83, A107, A125, A130, FUNCT_1:32
.= Fni1 . p by A115, A97, A111, A123, FUNCT_1:13 ;
:: thesis:

end;

A131: [:N1,S:] c= [:N2,S:] by A95, ZFMISC_1:96;
then reconsider K0 = [:N1,S:] as Subset of [:(Y | N2),(I[01] | S):] by A64, A60, PRE_TOPC:8;
A132: [:N1,SS:] c= dom F by A6, ZFMISC_1:96;
reconsider gF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],(Tunit_circle 2) by A97, A99, A111, FUNCT_2:2;
reconsider fF = F | [:N1,SS:] as Function of [:(Y | N1),(I[01] | SS):],((Tunit_circle 2) | Ui) by A98, A97, A99, A111, FUNCT_2:2;
[:(Y | N1),(I[01] | SS):] = [:Y,I[01]:] | [:N1,SS:] by BORSUK_3:22;
then gF is continuous by A3, TOPMETR:7;
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 A95, PRE_TOPC:8;
S c= S ;
then reconsider aS = S as non empty Subset of (I[01] | S) by PRE_TOPC:8;
[:(Y | N2),(I[01] | S):] | K0 = [:((Y | N2) | aN1),((I[01] | S) | aS):] by BORSUK_3:22
.= [:(Y | N1),((I[01] | S) | aS):] by GOBOARD9:2
.= [:(Y | N1),(I[01] | S):] by GOBOARD9:2 ;
then A135: Fn2 is continuous by A57, TOPMETR:7;
take N1 ; :: thesis:
take S1 = S \/ SS; :: thesis:
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 A103, BORSUK_1:def 2;
then reconsider Fn1 = Fn2 +* Fni1 as Function of [:(Y | N1),(I[01] | S1):],R^1 by A136, A113, A112, FUNCT_2:2, XBOOLE_1:1;
take Fn1 ; :: thesis:
thus A138: S1 = [.0,(TT . (i + 1)).] by A54, A62, A52, XXREAL_1:165; :: thesis:
0 <= TT . (i + 1) by A19, A32;
then 0 in S1 by A138, XXREAL_1:1;
then A139: {0} c= S1 by ZFMISC_1:31;
A140: dom (Fn1 | [: the carrier of Y,{0}:]) = (dom Fn1) /\ [: the carrier of Y,{0}:] by RELAT_1:61;
then A141: dom (Fn1 | [: the carrier of Y,{0}:]) = [:(N1 /\ the carrier of Y),(S1 /\ {0}):] by A136, A113, ZFMISC_1:100
.= [:N1,(S1 /\ {0}):] by XBOOLE_1:28
.= [:N1,{0}:] by A139, XBOOLE_1:28 ;
A142: for a being object st a in dom (Fn1 | [: the carrier of Y,{0}:]) holds
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a

proof

let a be object ; :: thesis:
A143: [:N1, the carrier of I[01]:] c= [:N2, the carrier of I[01]:] by A95, ZFMISC_1:96;
assume A144: a in dom (Fn1 | [: the carrier of Y,{0}:]) ; :: thesis:
then A145: a in [: the carrier of Y,{0}:] by A140, XBOOLE_0:def 4;
then consider a1, a2 being object such that
a1 in the carrier of Y and
A146: a2 in {0} and
A147: a = [a1,a2] by ZFMISC_1:def 2;
A148: a2 = 0 by A146, TARSKI:def 1;
0 in S by A54, A62, XXREAL_1:1;
then {0} c= S by ZFMISC_1:31;
then A149: [:N1,{0}:] c= [:N1,S:] by ZFMISC_1:96;
then A150: a in [:N1,S:] by A141, A144;
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 ;

suppose A153: not a in dom Fni1 ; :: thesis:

thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A145, FUNCT_1:49
.= (Fn | [:N1,S:]) . a by A153, FUNCT_4:11
.= Fn . a by A141, A144, A149, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . a by A59, A145, FUNCT_1:49
.= Ft . a by A152, A143, FUNCT_1:49
.= (Ft | [:N1, the carrier of I[01]:]) . a by A150, A151, FUNCT_1:49 ; :: thesis:

end;

suppose A154: a in dom Fni1 ; :: thesis:

set e = (Ft | [:N1, the carrier of I[01]:]) . a;
a in [:N1,SS:] by A6, A102, A154, RELAT_1:62, ZFMISC_1:96;
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 A147, A157, XTUPLE_0:1;
then A158: a2 = TT . i by A62, A148, A156, XXREAL_1:1;
a1 = b1 by A147, A157, XTUPLE_0:1;
then A159: ( [a1,(TT . i)] in [:N1,S:] & [a1,(TT . i)] in [:N1,{(TT . i)}:] ) by A63, A79, A155, ZFMISC_1:87;
(Ft | [:N1, the carrier of I[01]:]) . a = Ft . a by A150, A151, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . a by A152, A143, FUNCT_1:49
.= Fn . a by A59, A145, FUNCT_1:49 ;
then A160: (Ft | [:N1, the carrier of I[01]:]) . a in Fn .: [:N1,{(TT . i)}:] by A64, A60, A67, A61, A131, A147, A158, A159, FUNCT_1:def 6;
then A161: ff . ((Ft | [:N1, the carrier of I[01]:]) . a) = CircleMap . ((Ft | [:N1, the carrier of I[01]:]) . a) by A117, FUNCT_1:49
.= CircleMap . (Ft . a) by A150, A151, FUNCT_1:49
.= (CircleMap * Ft) . a by A8, A145, FUNCT_1:13
.= F . a by A5, A145, FUNCT_1:49 ;
thus (Fn1 | [: the carrier of Y,{0}:]) . a = Fn1 . a by A145, FUNCT_1:49
.= Fni1 . a by A154, FUNCT_4:13
.= (ff ") . ((F | [:N1,SS:]) . a) by A115, A102, A154, FUNCT_1:13
.= (ff ") . (F . a) by A97, A102, A154, FUNCT_1:49
.= (Ft | [:N1, the carrier of I[01]:]) . a by A117, A83, A107, A160, A161, FUNCT_1:32 ; :: thesis:

end;

A162: rng Fn1 c= dom CircleMap by Lm12, TOPMETR:17;
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:
assume A165: a in dom (CircleMap * Fn1) ; :: thesis:

per cases ;

suppose A166: a in dom Fni1 ; :: thesis:

A167: [:N1,SS:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
A168: a in [:N1,SS:] by A6, A102, A166, RELAT_1:62, ZFMISC_1:96;
then F . a in F .: [:N1,SS:] by A6, A167, FUNCT_1:def 6;
then A169: F . a in F .: [:N,SS:] by A96;
then a in F " (dom (ff ")) by A6, A48, A51, A98, A115, A168, A167, FUNCT_1:def 7;
then A170: a in dom ((ff ") * F) by RELAT_1:147;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A165, FUNCT_2:15
.= CircleMap . (Fni1 . a) by A166, FUNCT_4:13
.= CircleMap . ((f ") . ((F | [:N1,SS:]) . a)) by A102, A166, FUNCT_1:13
.= CircleMap . ((f ") . (F . a)) by A97, A102, A166, FUNCT_1:49
.= CircleMap . (((ff ") * F) . a) by A132, A115, A97, A102, A166, FUNCT_1:13
.= (CircleMap * ((ff ") * F)) . a by A170, FUNCT_1:13
.= ((CircleMap * (ff ")) * F) . a by RELAT_1:36
.= (CircleMap * (ff ")) . (F . a) by A132, A97, A102, A166, FUNCT_1:13
.= F . a by A48, A51, A114, A107, A169, TOPALG_3:2 ; :: thesis:

end;

suppose A171: not a in dom Fni1 ; :: thesis:

then A172: a in [:N1,S:] by A97, A102, A113, A163, A165, XBOOLE_0:def 3;
thus (CircleMap * Fn1) . a = CircleMap . (Fn1 . a) by A165, FUNCT_2:15
.= CircleMap . ((Fn | [:N1,S:]) . a) by A171, FUNCT_4:11
.= CircleMap . (Fn . a) by A172, FUNCT_1:49
.= (CircleMap * Fn) . a by A64, A60, A67, A131, A172, FUNCT_2:15
.= F . a by A58, A131, A172, FUNCT_1:49 ; :: thesis:

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 A64, A137, TSEP_1:4;
A175: SS c= S1 by XBOOLE_1:7;
then reconsider F1 = [#] (I[01] | S), F2 = [#] (I[01] | SS) as Subset of (I[01] | S1) by A137, A173, PRE_TOPC:8;
reconsider hS = F1, hSS = F2 as Subset of I[01] by PRE_TOPC:8;
hS is closed by A54, BORSUK_4:23, PRE_TOPC:8;
then A176: F1 is closed by TSEP_1:8;
thus y in N1 by A55, A94, XBOOLE_0:def 4; :: thesis:
thus N1 c= N by A56, A95; :: thesis:
hSS is closed by BORSUK_4:23, PRE_TOPC:8;
then A177: F2 is closed by TSEP_1:8;
I[01] | SS is SubSpace of I[01] | S1 by A110, A137, A175, TSEP_1:4;
then ex h being Function of [:(Y | N1),(I[01] | S1):],R^1 st
( h = Fn2 +* Fni1 & h is continuous ) by A64, A110, A137, A174, A176, A177, A135, A134, A121, TOPALG_3:19;
hence Fn1 is continuous ; :: thesis:
dom Fn1 = (dom F) /\ [:N1,S1:] by A6, A136, A113, XBOOLE_1:28, ZFMISC_1:96;
hence F | [:N1,S1:] = CircleMap * Fn1 by A162, A164, FUNCT_1:46, RELAT_1:27; :: thesis:
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),({0} /\ the carrier of I[01]):] by A8, ZFMISC_1:100
.= [:N1,({0} /\ the carrier of I[01]):] by XBOOLE_1:28
.= [:N1,{0}:] by Lm3, XBOOLE_1:28 ;
hence Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] by A141, A142; :: thesis:

end;

A178: S₂[ 0 ] by FINSEQ_3:24;
for i being Nat holds S₂[i] from NAT_1:sch 2(A178, A30);
then consider N2 being non empty open Subset of Y, S being non empty Subset of I[01], Fn1 being Function of [:(Y | N2),(I[01] | S):],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,{0}:] = 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 A12, A179, Lm6, BORSUK_1:40, TSEP_1:3;
then reconsider Fn1 = Fn1 as Function of [:(Y | N2),I[01]:],R^1 ;
take z ; :: thesis:
take y ; :: thesis:
take t ; :: thesis:
take N2 ; :: thesis:
take Fn1 ; :: thesis:
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,{0}:] = Ft | [:N2, the carrier of I[01]:] ) by A10, A12, A179, A180, A182, A183, A184, A185, BORSUK_1:40; :: thesis:
let H be Function of [:(Y | N2),I[01]:],R^1; :: thesis:
assume that
A186: H is continuous and
A187: F | [:N2, the carrier of I[01]:] = CircleMap * H and
A188: H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ; :: thesis:
defpred S₃[ 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 BORSUK_1:def 2, PRE_TOPC:8;
A191: dom H = the carrier of [:(Y | N2),I[01]:] by FUNCT_2:def 1;
A192: for i being Nat st S₃[i] holds
S₃[i + 1]

proof

let i be Nat; :: thesis:
assume that
A193: S₃[i] and
A194: i + 1 in dom TT ; :: thesis:

per cases by A194, TOPREALA:2;

suppose A195: i = 0 ; :: thesis:

set Z = [.0,(TT . (i + 1)).];
A196: [.0,(TT . (i + 1)).] = {0} by A11, A195, XXREAL_1:17;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A11, A195, Lm3, XXREAL_1:17;
A197: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A198: dom (Fn1 | [:N2,Z:]) = [:N2,Z:] by A190, A189, RELAT_1:62;
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:
A200: [:N2,Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A201: x in dom (Fn1 | [:N2,Z:]) ; :: thesis:
hence (Fn1 | [:N2,Z:]) . x = Fn1 . x by A198, FUNCT_1:49
.= (Fn1 | [: the carrier of Y,{0}:]) . x by A196, A198, A201, A200, FUNCT_1:49
.= H . x by A184, A188, A196, A198, A201, A200, FUNCT_1:49
.= (H | [:N2,Z:]) . x by A198, A201, FUNCT_1:49 ;
:: thesis:

end;

take Z ; :: thesis:
thus Z = [.0,(TT . (i + 1)).] ; :: thesis:
dom (H | [:N2,Z:]) = [:N2,Z:] by A191, A190, A197, RELAT_1:62;
hence Fn1 | [:N2,Z:] = H | [:N2,Z:] by A189, A199, RELAT_1:62; :: thesis:

end;

suppose A202: i in dom TT ; :: thesis:

set ZZ = [.(TT . i),(TT . (i + 1)).];
A203: 0 <= TT . i by A19, A202;
A204: TT . (i + 1) <= 1 by A19, A194, A202;
then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A25, A203;
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 A193, A202;
take Z1 = Z \/ ZZ; :: thesis:
A207: TT . i < TT . (i + 1) by A19, A194, A202;
hence Z1 = [.0,(TT . (i + 1)).] by A205, A203, XXREAL_1:165; :: thesis:
A208: [:N2,Z1:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then A209: dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:] by A190, A189, RELAT_1:62;
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 A19, A194;
then A211: TT . (i + 1) is Point of I[01] by A204, BORSUK_1:43;
( 0 <= TT . i & TT . i <= 1 ) by A19, A194, A202;
then TT . i is Point of I[01] by BORSUK_1:43;
then A212: ZZ is connected by A207, A211, BORSUK_4:24;
consider Ui being non empty Subset of (Tunit_circle 2) such that
A213: Ui in UL and
A214: F .: [:N,ZZ:] c= Ui by A16, A194, A202;
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),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A213;
let x be object ; :: thesis:
assume A217: x in dom (Fn1 | [:N2,Z1:]) ; :: thesis:
consider x1, x2 being object such that
A218: x1 in N2 and
A219: x2 in Z1 and
A220: x = [x1,x2] by A209, A217, ZFMISC_1:def 2;
A221: TT . i in ZZ by A207, XXREAL_1:1;
then [x1,(TT . i)] in [:N,ZZ:] by A181, A218, ZFMISC_1:87;
then A222: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
reconsider xy = {x1} as non empty Subset of Y by A218, ZFMISC_1:31;
A223: xy c= N2 by A218, ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A190, ZFMISC_1:96;
A224: dom (H | [:xy,ZZ:]) = [:xy,ZZ:] by A191, A190, A223, RELAT_1:62, ZFMISC_1:96;
A225: D is Cover of Fn1 .: xZZ

proof

let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
A226: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; :: thesis:
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 A181, A218, ZFMISC_1:31;
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 A6, A226, FUNCT_1:def 6;
CircleMap . (Fn1 . a) = (CircleMap * Fn1) . a by FUNCT_2:15
.= F . a by A12, A179, A183, A190, BORSUK_1:40, FUNCT_1:49 ;
hence b in union D by A214, A215, A228, A229, Lm12, FUNCT_1:def 7, TOPMETR:17; :: thesis:

end;

A230: D is Cover of H .: xZZ

proof

let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
A231: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in H .: xZZ ; :: thesis:
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) = (CircleMap * H) . a by FUNCT_2:15
.= F . a by A187, A190, FUNCT_1:49 ;
xy c= N by A181, A218, ZFMISC_1:31;
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 A6, A231, FUNCT_1:def 6;
hence b in union D by A214, A215, A233, A234, Lm12, FUNCT_1:def 7, TOPMETR:17; :: thesis:

end;

A235: H . [x1,(TT . i)] in REAL by XREAL_0:def 1;
TT . i in Z by A205, A203, XXREAL_1:1;
then A236: [x1,(TT . i)] in [:N2,Z:] by A218, ZFMISC_1:87;
then A237: Fn1 . [x1,(TT . i)] = (Fn1 | [:N2,Z:]) . [x1,(TT . i)] by FUNCT_1:49
.= H . [x1,(TT . i)] by A206, A236, FUNCT_1:49 ;
A238: [:N2,Z:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:95;
then F . [x1,(TT . i)] = (CircleMap * H) . [x1,(TT . i)] by A187, A236, FUNCT_1:49
.= CircleMap . (H . [x1,(TT . i)]) by A191, A190, A236, A238, FUNCT_1:13 ;
then H . [x1,(TT . i)] in CircleMap " Ui by A214, A222, FUNCT_2:38, A235, TOPMETR:17;
then consider Uith being set such that
A239: H . [x1,(TT . i)] in Uith and
A240: Uith in D by A215, TARSKI:def 4;
A241: Fn1 . [x1,(TT . i)] in REAL by XREAL_0:def 1;
F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A12, A179, A183, A236, A238, BORSUK_1:40, FUNCT_1:49
.= CircleMap . (Fn1 . [x1,(TT . i)]) by A190, A189, A236, A238, FUNCT_1:13 ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A214, A222, FUNCT_2:38, A241, TOPMETR:17;
then consider Uit being set such that
A242: Fn1 . [x1,(TT . i)] in Uit and
A243: Uit in D by A215, TARSKI:def 4;
I[01] is SubSpace of I[01] by TSEP_1:2;
then A244: [:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21;
xy is connected by A218;
then [:xy,ZZ:] is connected by A212, TOPALG_3:16;
then A245: xZZ is connected by A244, CONNSP_1:23;
reconsider Uith = Uith as non empty Subset of R^1 by A239, A240;
A246: x1 in xy by TARSKI:def 1;
then A247: [x1,(TT . i)] in xZZ by A221, ZFMISC_1:87;
then H . [x1,(TT . i)] in H .: xZZ by FUNCT_2:35;
then Uith meets H .: xZZ by A239, XBOOLE_0:3;
then A248: H .: xZZ c= Uith by A186, A245, A240, A230, TOPALG_3:12, TOPS_2:61;
reconsider Uit = Uit as non empty Subset of R^1 by A242, A243;
set f = CircleMap | Uit;
A249: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A250: rng (CircleMap | Uit) c= Ui

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (CircleMap | Uit) ; :: thesis:
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 A243, A249, A251, TARSKI:def 4;
then CircleMap . a in Ui by A215, FUNCT_2:38;
hence b in Ui by A249, A251, A252, FUNCT_1:49; :: thesis:

end;

( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A249, A250, FUNCT_2:2;
A253: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A190, A189, A223, RELAT_1:62, ZFMISC_1:96;
H . [x1,(TT . i)] in H .: xZZ by A191, A247, FUNCT_1:def 6;
then Uit meets Uith by A242, A248, A237, XBOOLE_0:3;
then A254: Uit = Uith by A243, A240, TAXONOM2:def 5;
A255: rng (H | [:xy,ZZ:]) c= dom f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (H | [:xy,ZZ:]) ; :: thesis:
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 A224, A256, A257, FUNCT_1:49;
then b in H .: xZZ by A191, A224, A256, FUNCT_1:def 6;
hence b in dom f by A248, A254, A249; :: thesis:

end;

Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by A247, FUNCT_2:35;
then Uit meets Fn1 .: xZZ by A242, XBOOLE_0:3;
then A258: Fn1 .: xZZ c= Uit by A182, A185, A243, A245, A225, TOPALG_3:12, TOPS_2:61;
A259: rng (Fn1 | [:xy,ZZ:]) c= dom f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (Fn1 | [:xy,ZZ:]) ; :: thesis:
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 A253, A260, A261, FUNCT_1:49;
then b in Fn1 .: xZZ by A189, A253, A260, FUNCT_1:def 6;
hence b in dom f by A258, A249; :: thesis:

end;

proof

let x be object ; :: thesis:
assume A264: x in dom (f * (Fn1 | [:xy,ZZ:])) ; :: thesis:
A265: Fn1 . x in Fn1 .: [:xy,ZZ:] by A189, A253, A262, A264, FUNCT_1:def 6;
A266: H . x in H .: [:xy,ZZ:] by A191, A253, A262, A264, FUNCT_1:def 6;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by A253, A262, A264, FUNCT_1:49
.= f . (Fn1 . x) by A189, A264, FUNCT_1:13
.= CircleMap . (Fn1 . x) by A258, A265, FUNCT_1:49
.= (CircleMap * Fn1) . x by A189, A264, FUNCT_1:13
.= CircleMap . (H . x) by A12, A179, A183, A187, A191, A264, BORSUK_1:40, FUNCT_1:13
.= f . (H . x) by A248, A254, A266, FUNCT_1:49
.= (f * H) . x by A191, A264, FUNCT_1:13
.= ((f * H) | [:xy,ZZ:]) . x by A253, A262, A264, FUNCT_1:49
.= (f * (H | [:xy,ZZ:])) . x by RELAT_1:83 ; :: thesis:

end;

f is being_homeomorphism by A216, A243;
then A267: f is one-to-one ;
dom (f * (H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:]) by A255, RELAT_1:27;
then A268: f * (Fn1 | [:xy,ZZ:]) = f * (H | [:xy,ZZ:]) by A253, A224, A259, A263, RELAT_1:27;

per cases ;

suppose x2 in ZZ ; :: thesis:

then A269: x in [:xy,ZZ:] by A220, A246, ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A209, A217, FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]) . x by A269, FUNCT_1:49
.= (H | [:xy,ZZ:]) . x by A267, A253, A224, A259, A255, A268, FUNCT_1:27
.= H . x by A269, FUNCT_1:49
.= (H | [:N2,Z1:]) . x by A209, A217, FUNCT_1:49 ; :: thesis:

end;

suppose not x2 in ZZ ; :: thesis:

then x2 in Z by A219, XBOOLE_0:def 3;
then A270: x in [:N2,Z:] by A218, A220, ZFMISC_1:87;
thus (Fn1 | [:N2,Z1:]) . x = Fn1 . x by A209, A217, FUNCT_1:49
.= (Fn1 | [:N2,Z:]) . x by A270, FUNCT_1:49
.= H . x by A206, A270, FUNCT_1:49
.= (H | [:N2,Z1:]) . x by A209, A217, FUNCT_1:49 ; :: thesis:

end;

dom (H | [:N2,Z1:]) = [:N2,Z1:] by A191, A190, A208, RELAT_1:62;
hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by A189, A210, RELAT_1:62; :: thesis:

end;

A271: S₃[ 0 ] by FINSEQ_3:24;
for i being Nat holds S₃[i] from NAT_1:sch 2(A271, A192);
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 A12, A190, A189, A272, BORSUK_1:40, RELAT_1:69
.= H by A12, A191, A190, A272, A273, BORSUK_1:40, RELAT_1:69 ; :: thesis:

end;

consider G being Function of [:Y,I[01]:],R^1 such that
A274: for x being Point of [:Y,I[01]:] holds S₁[x,G . x] from FUNCT_2:sch 3(A9);
take G ; :: thesis:

A275: now :: thesis:

let N be Subset of Y; :: thesis:
let F be Function of [:(Y | N),I[01]:],R^1; :: thesis:
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:

end;

A276: for p being Point of [:Y,I[01]:]
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,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = 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 [:Y,I[01]:]; :: thesis:
let y be Point of Y; :: thesis:
let t be Point of I[01]; :: thesis:
let N1, N2 be non empty open Subset of Y; :: thesis:
let Fn1 be Function of [:(Y | N1),I[01]:],R^1; :: thesis:
let Fn2 be Function of [:(Y | N2),I[01]:],R^1; :: thesis:
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,{0}:] = 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,{0}:] = Ft | [:N1, the carrier of I[01]:] ; :: thesis:
A285: {y} c= N1 by A277, ZFMISC_1:31;
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 (Tunit_circle 2) 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 (Tunit_circle 2) 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 S₂[ 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 A278, ZFMISC_1:31;
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 BORSUK_1:def 2, PRE_TOPC:8;
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 BORSUK_1:def 2, PRE_TOPC:8;
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 S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis:
assume that
A302: S₂[i] and
A303: i + 1 in dom TT ; :: thesis:

per cases by A303, TOPREALA:2;

suppose A304: i = 0 ; :: thesis:

set Z = [.0,(TT . (i + 1)).];
A305: [.0,(TT . (i + 1)).] = {0} by A286, A304, XXREAL_1:17;
reconsider Z = [.0,(TT . (i + 1)).] as non empty Subset of I[01] by A286, A304, Lm3, XXREAL_1:17;
A306: [:{y},Z:] c= [:N2, the carrier of I[01]:] by A295, ZFMISC_1:96;
A307: dom (Fn1 | [:{y},Z:]) = [:{y},Z:] by A285, A298, RELAT_1:62, ZFMISC_1:96;
A308: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A285, ZFMISC_1:96;
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:
A310: [:{y},Z:] c= [: the carrier of Y,Z:] by ZFMISC_1:95;
assume A311: x in dom (Fn1 | [:{y},Z:]) ; :: thesis:
hence (Fn1 | [:{y},Z:]) . x = Fn1 . x by A307, FUNCT_1:49
.= (Fn1 | [: the carrier of Y,{0}:]) . x by A305, A307, A311, A310, FUNCT_1:49
.= Ft . x by A284, A308, A307, A311, FUNCT_1:49
.= (Ft | [:N2, the carrier of I[01]:]) . x by A307, A306, A311, FUNCT_1:49
.= Fn2 . x by A282, A305, A307, A311, A310, FUNCT_1:49
.= (Fn2 | [:{y},Z:]) . x by A307, A311, FUNCT_1:49 ;
:: thesis:

end;

take Z ; :: thesis:
thus Z = [.0,(TT . (i + 1)).] ; :: thesis:
dom (Fn2 | [:{y},Z:]) = [:{y},Z:] by A295, A294, RELAT_1:62, ZFMISC_1:96;
hence Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] by A307, A309; :: thesis:

end;

suppose A312: i in dom TT ; :: thesis:

A313: now :: thesis:

let i be Element of NAT ; :: thesis:
assume A314: i in dom TT ; :: thesis:
1 <= i by A314, FINSEQ_3:25;
then ( 1 = i or 1 < i ) by XXREAL_0:1;
hence A315: 0 <= TT . i by A286, A288, A300, A314, SEQM_3:def 1; :: thesis:
assume A316: i + 1 in dom TT ; :: thesis:
A317: i + 0 < i + 1 by XREAL_1:8;
hence A318: TT . i < TT . (i + 1) by A288, A314, A316, SEQM_3:def 1; :: thesis:
i + 1 <= len TT by A316, FINSEQ_3:25;
then ( i + 1 = len TT or i + 1 < len TT ) by XXREAL_0:1;
hence TT . (i + 1) <= 1 by A287, A288, A292, A316, SEQM_3:def 1; :: thesis:
hence TT . i < 1 by A318, XXREAL_0:2; :: thesis:
thus 0 < TT . (i + 1) by A288, A314, A315, A316, A317, SEQM_3:def 1; :: thesis:

end;

then A319: 0 <= TT . i by A312;
A320: TT . (i + 1) <= 1 by A303, A312, A313;
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 A302, A312;

now :: thesis:

let i be Nat; :: thesis:
assume that
A323: 0 <= TT . i and
A324: TT . (i + 1) <= 1 ; :: thesis:
thus [.(TT . i),(TT . (i + 1)).] c= the carrier of I[01] :: thesis:

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume A325: a in [.(TT . i),(TT . (i + 1)).] ; :: thesis:
then reconsider a = a as Real ;
a <= TT . (i + 1) by A325, XXREAL_1:1;
then A326: a <= 1 by A324, XXREAL_0:2;
0 <= a by A323, A325, XXREAL_1:1;
hence a in the carrier of I[01] by A326, BORSUK_1:43; :: thesis:

end;

then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A319, A320;
take Z1 = Z \/ ZZ; :: thesis:
A327: TT . i < TT . (i + 1) by A303, A312, A313;
hence Z1 = [.0,(TT . (i + 1)).] by A321, A319, XXREAL_1:165; :: thesis:
A328: dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:] by A285, A298, RELAT_1:62, ZFMISC_1:96;
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 A303, A313;
then A330: TT . (i + 1) is Point of I[01] by A320, BORSUK_1:43;
( 0 <= TT . i & TT . i <= 1 ) by A303, A312, A313;
then TT . i is Point of I[01] by BORSUK_1:43;
then A331: ZZ is connected by A327, A330, BORSUK_4:24;
A332: TT . i in ZZ by A327, XXREAL_1:1;
consider Ui being non empty Subset of (Tunit_circle 2) such that
A333: Ui in UL and
A334: F .: [:N,ZZ:] c= Ui by A291, A303, A312;
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),((Tunit_circle 2) | Ui) st f = CircleMap | d holds
f is being_homeomorphism by A2, A333;
let x be object ; :: thesis:
assume A337: x in dom (Fn1 | [:{y},Z1:]) ; :: thesis:
consider x1, x2 being object such that
A338: x1 in {y} and
A339: x2 in Z1 and
A340: x = [x1,x2] by A328, A337, ZFMISC_1:def 2;
reconsider xy = {x1} as non empty Subset of Y by A338, ZFMISC_1:31;
A341: xy c= N2 by A295, A338, ZFMISC_1:31;
then A342: [:xy,ZZ:] c= [:N2, the carrier of I[01]:] by ZFMISC_1:96;
A343: x1 = y by A338, TARSKI:def 1;
then [x1,(TT . i)] in [:N,ZZ:] by A290, A332, ZFMISC_1:87;
then A344: F . [x1,(TT . i)] in F .: [:N,ZZ:] by FUNCT_2:35;
A345: xy c= N1 by A285, A338, ZFMISC_1:31;
then reconsider xZZ = [:xy,ZZ:] as Subset of [:(Y | N1),I[01]:] by A296, ZFMISC_1:96;
xy is connected by A338;
then A346: [:xy,ZZ:] is connected by A331, TOPALG_3:16;
A347: xy c= N by A290, A343, ZFMISC_1:31;
A348: D is Cover of Fn1 .: xZZ

proof

let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
A349: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn1 .: xZZ ; :: thesis:
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 A283, A296, FUNCT_1:49 ;
[:xy,ZZ:] c= [:N,ZZ:] by A347, ZFMISC_1:95;
then a in [:N,ZZ:] by A350;
then F . a in F .: [:N,ZZ:] by A6, A349, FUNCT_1:def 6;
hence b in union D by A334, A335, A351, A352, Lm12, FUNCT_1:def 7, TOPMETR:17; :: thesis:

end;

A353: I[01] is SubSpace of I[01] by TSEP_1:2;
then [:(Y | N1),I[01]:] is SubSpace of [:Y,I[01]:] by BORSUK_3:21;
then A354: xZZ is connected by A346, CONNSP_1:23;
reconsider XZZ = [:xy,ZZ:] as Subset of [:(Y | N2),I[01]:] by A297, A341, ZFMISC_1:96;
[:(Y | N2),I[01]:] is SubSpace of [:Y,I[01]:] by A353, BORSUK_3:21;
then A355: XZZ is connected by A346, CONNSP_1:23;
A356: D is Cover of Fn2 .: xZZ

proof

let b be object ; :: according to TARSKI:def 3,SETFAM_1:def 11 :: thesis:
A357: [:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:] by ZFMISC_1:96;
assume b in Fn2 .: xZZ ; :: thesis:
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 A281, A297, FUNCT_1:49 ;
[:xy,ZZ:] c= [:N,ZZ:] by A347, ZFMISC_1:95;
then a in [:N,ZZ:] by A358;
then F . a in F .: [:N,ZZ:] by A6, A357, FUNCT_1:def 6;
hence b in union D by A334, A335, A359, A360, Lm12, FUNCT_1:def 7, TOPMETR:17; :: thesis:

end;

A361: TT . i in Z by A321, A319, XXREAL_1:1;
then A362: [x1,(TT . i)] in [:{y},Z:] by A338, ZFMISC_1:87;
A363: Fn1 . [x1,(TT . i)] in REAL by XREAL_0:def 1;
A364: [:{y},Z:] c= [:N1, the carrier of I[01]:] by A285, ZFMISC_1:96;
then F . [x1,(TT . i)] = (CircleMap * Fn1) . [x1,(TT . i)] by A283, A362, FUNCT_1:49
.= CircleMap . (Fn1 . [x1,(TT . i)]) by A298, A362, A364, FUNCT_1:13 ;
then Fn1 . [x1,(TT . i)] in CircleMap " Ui by A334, A344, FUNCT_2:38, A363, TOPMETR:17;
then consider Uit being set such that
A365: Fn1 . [x1,(TT . i)] in Uit and
A366: Uit in D by A335, TARSKI:def 4;
reconsider Uit = Uit as non empty Subset of R^1 by A365, A366;
set f = CircleMap | Uit;
A367: dom (CircleMap | Uit) = Uit by Lm12, RELAT_1:62, TOPMETR:17;
A368: rng (CircleMap | Uit) c= Ui

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (CircleMap | Uit) ; :: thesis:
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 A366, A367, A369, TARSKI:def 4;
then CircleMap . a in Ui by A335, FUNCT_2:38;
hence b in Ui by A367, A369, A370, FUNCT_1:49; :: thesis:

end;

( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit ) by PRE_TOPC:8;
then reconsider f = CircleMap | Uit as Function of (R^1 | Uit),((Tunit_circle 2) | Ui) by A367, A368, FUNCT_2:2;
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 A295, A338, A361, ZFMISC_1:87;
then F . [x1,(TT . i)] = (CircleMap * Fn2) . [x1,(TT . i)] by A281, A371, FUNCT_1:49
.= CircleMap . (Fn2 . [x1,(TT . i)]) by A293, A297, A373, A371, FUNCT_1:13 ;
then Fn2 . [x1,(TT . i)] in CircleMap " Ui by A334, A344, FUNCT_2:38, A372, TOPMETR:17;
then consider Uith being set such that
A374: Fn2 . [x1,(TT . i)] in Uith and
A375: Uith in D by A335, TARSKI:def 4;
reconsider Uith = Uith as non empty Subset of R^1 by A374, A375;
A376: dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:] by A296, A299, A345, RELAT_1:62, ZFMISC_1:96;
A377: x1 in xy by TARSKI:def 1;
then A378: [x1,(TT . i)] in xZZ by A332, ZFMISC_1:87;
then Fn1 . [x1,(TT . i)] in Fn1 .: xZZ by FUNCT_2:35;
then Uit meets Fn1 .: xZZ by A365, XBOOLE_0:3;
then A379: Fn1 .: xZZ c= Uit by A280, A366, A354, A348, TOPALG_3:12, TOPS_2:61;
A380: rng (Fn1 | [:xy,ZZ:]) c= dom f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (Fn1 | [:xy,ZZ:]) ; :: thesis:
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 A376, A381, A382, FUNCT_1:49;
then b in Fn1 .: xZZ by A299, A376, A381, FUNCT_1:def 6;
hence b in dom f by A379, A367; :: thesis:

end;

then A383: dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:]) by RELAT_1:27;
[x1,(TT . i)] in [:xy,ZZ:] by A338, A343, A332, ZFMISC_1:87;
then [x1,(TT . i)] in dom Fn2 by A294, A342;
then A384: Fn2 . [x1,(TT . i)] in Fn2 .: xZZ by A378, FUNCT_2:35;
then Uith meets Fn2 .: xZZ by A374, XBOOLE_0:3;
then A385: Fn2 .: xZZ c= Uith by A279, A375, A355, A356, TOPALG_3:12, TOPS_2:61;
Fn1 . [x1,(TT . i)] = (Fn1 | [:{y},Z:]) . [x1,(TT . i)] by A362, FUNCT_1:49
.= Fn2 . [x1,(TT . i)] by A322, A362, FUNCT_1:49 ;
then Uit meets Uith by A365, A384, A385, XBOOLE_0:3;
then A386: Uit = Uith by A366, A375, TAXONOM2:def 5;
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:
assume A389: x in dom (f * (Fn1 | [:xy,ZZ:])) ; :: thesis:
A390: Fn1 . x in Fn1 .: [:xy,ZZ:] by A299, A376, A383, A389, FUNCT_1:def 6;
A391: Fn2 . x in Fn2 .: [:xy,ZZ:] by A294, A342, A376, A383, A389, FUNCT_1:def 6;
dom (Fn1 | [:xy,ZZ:]) = (dom Fn1) /\ [:xy,ZZ:] by RELAT_1:61;
then A392: x in [:xy,ZZ:] by A383, A389, XBOOLE_0:def 4;
thus (f * (Fn1 | [:xy,ZZ:])) . x = ((f * Fn1) | [:xy,ZZ:]) . x by RELAT_1:83
.= (f * Fn1) . x by A376, A383, A389, FUNCT_1:49
.= f . (Fn1 . x) by A299, A389, FUNCT_1:13
.= CircleMap . (Fn1 . x) by A379, A390, FUNCT_1:49
.= (CircleMap * Fn1) . x by A299, A389, FUNCT_1:13
.= F . x by A283, A298, A383, A389, A388, FUNCT_1:49
.= (CircleMap * Fn2) . x by A281, A342, A392, FUNCT_1:49
.= CircleMap . (Fn2 . x) by A294, A342, A392, FUNCT_1:13
.= f . (Fn2 . x) by A385, A386, A391, FUNCT_1:49
.= (f * Fn2) . x by A294, A342, A392, FUNCT_1:13
.= ((f * Fn2) | [:xy,ZZ:]) . x by A376, A383, A389, FUNCT_1:49
.= (f * (Fn2 | [:xy,ZZ:])) . x by RELAT_1:83 ; :: thesis:

end;

A393: dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:] by A293, A297, A341, RELAT_1:62, ZFMISC_1:96;
A394: rng (Fn2 | [:xy,ZZ:]) c= dom f

proof

let b be object ; :: according to TARSKI:def 3 :: thesis:
assume b in rng (Fn2 | [:xy,ZZ:]) ; :: thesis:
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 A393, A395, A396, FUNCT_1:49;
then b in Fn2 .: xZZ by A293, A393, A395, FUNCT_1:def 6;
hence b in dom f by A385, A386, A367; :: thesis:

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 A376, A393, A380, A387, RELAT_1:27;
f is being_homeomorphism by A336, A366;
then A398: f is one-to-one ;

per cases ;

suppose x2 in ZZ ; :: thesis:

then A399: x in [:xy,ZZ:] by A340, A377, ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A328, A337, FUNCT_1:49
.= (Fn1 | [:xy,ZZ:]) . x by A399, FUNCT_1:49
.= (Fn2 | [:xy,ZZ:]) . x by A398, A376, A393, A380, A394, A397, FUNCT_1:27
.= Fn2 . x by A399, FUNCT_1:49
.= (Fn2 | [:{y},Z1:]) . x by A328, A337, FUNCT_1:49 ; :: thesis:

end;

suppose not x2 in ZZ ; :: thesis:

then x2 in Z by A339, XBOOLE_0:def 3;
then A400: x in [:{y},Z:] by A338, A340, ZFMISC_1:87;
thus (Fn1 | [:{y},Z1:]) . x = Fn1 . x by A328, A337, FUNCT_1:49
.= (Fn1 | [:{y},Z:]) . x by A400, FUNCT_1:49
.= Fn2 . x by A322, A400, FUNCT_1:49
.= (Fn2 | [:{y},Z1:]) . x by A328, A337, FUNCT_1:49 ; :: thesis:

end;

dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:] by A295, A293, A297, RELAT_1:62, ZFMISC_1:96;
hence Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] by A328, A329; :: thesis:

end;

A401: S₂[ 0 ] by FINSEQ_3:24;
for i being Nat holds S₂[i] from NAT_1:sch 2(A401, A301);
then ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (len TT)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] ) by A292;
hence Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:] by A287, BORSUK_1:40; :: thesis:

end;

for p being Point of [:Y,I[01]:]
for V being Subset of R^1 st G . p in V & V is open holds
ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V )

proof

let p be Point of [:Y,I[01]:]; :: thesis:
let V be Subset of R^1; :: thesis:
assume A402: ( G . p in V & V is open ) ; :: thesis:
consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:(Y | N),I[01]:],R^1 such that
A403: p = [y,t] and
A404: G . p = Fn . p and
A405: y in N and
A406: Fn is continuous and
A407: ( F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] ) and
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,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A274;
A408: the carrier of [:(Y | N),I[01]:] = [: 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 ;
then p in the carrier of [:(Y | N),I[01]:] by A403, A405, ZFMISC_1:87;
then consider W being Subset of [:(Y | N),I[01]:] such that
A409: p in W and
A410: W is open and
A411: Fn .: W c= V by A402, A404, A406, JGRAPH_2:10;
A412: dom Fn = [:N, the carrier of I[01]:] by A408, FUNCT_2:def 1;
A413: [#] (Y | N) = N by PRE_TOPC:def 5;
then A414: [#] [:(Y | N),I[01]:] = [:N,([#] I[01]):] by BORSUK_3:1;
[:(Y | N),I[01]:] = [:Y,I[01]:] | [:N,([#] I[01]):] by Lm7, BORSUK_3:22;
then consider C being Subset of [:Y,I[01]:] such that
A415: C is open and
A416: C /\ ([#] [:(Y | N),I[01]:]) = W by A410, TOPS_2:24;
take WW = C /\ [:N,([#] I[01]):]; :: thesis:
thus p in WW by A409, A416, A413, BORSUK_3:1; :: thesis:
[:N,([#] I[01]):] is open by BORSUK_1:6;
hence WW is open by A415; :: thesis:
let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in G .: WW ; :: thesis:
then consider x being Point of [:Y,I[01]:] such that
A417: x in WW and
A418: y = G . x by FUNCT_2:65;
consider y0 being Point of Y, t0 being Point of I[01], N0 being non empty open Subset of Y, Fn0 being Function of [:(Y | N0),I[01]:],R^1 such that
A419: x = [y0,t0] and
A420: G . x = Fn0 . x and
A421: ( y0 in N0 & Fn0 is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * Fn0 & Fn0 | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] ) and
for H being Function of [:(Y | N0),I[01]:],R^1 st H is continuous & F | [:N0, the carrier of I[01]:] = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] holds
Fn0 = H by A274;
x in [:N,([#] I[01]):] by A417, XBOOLE_0:def 4;
then A422: y0 in N by A419, ZFMISC_1:87;
A423: x in [:{y0}, the carrier of I[01]:] by A419, ZFMISC_1:105;
then Fn . x = (Fn | [:{y0}, the carrier of I[01]:]) . x by FUNCT_1:49
.= (Fn0 | [:{y0}, the carrier of I[01]:]) . x by A276, A406, A407, A419, A421, A422
.= Fn0 . x by A423, FUNCT_1:49 ;
then y in Fn .: W by A412, A416, A414, A417, A418, A420, FUNCT_1:def 6;
hence y in V by A411; :: thesis:

end;

hence G is continuous by JGRAPH_2:10; :: thesis:
for x being Point of [:Y,I[01]:] holds F . x = (CircleMap * G) . x

proof

end;

hence F = CircleMap * G ; :: thesis:
A430: [: the carrier of Y,{0}:] c= [: the carrier of Y, the carrier of I[01]:] by Lm3, ZFMISC_1:95;
A431: the carrier of [:Y,I[01]:] = [: the carrier of Y, the carrier of I[01]:] by BORSUK_1:def 2;
then A432: dom G = [: the carrier of Y, the carrier of I[01]:] by FUNCT_2:def 1;
A433: for x being object st x in dom Ft holds
Ft . x = G . x

proof

let x be object ; :: thesis:
assume A434: x in dom Ft ; :: thesis:
then x in dom G by A8, A432, A430;
then consider y being Point of Y, t being Point of I[01], N being non empty open Subset of Y, Fn being Function of [:(Y | N),I[01]:],R^1 such that
A435: x = [y,t] and
A436: G . x = Fn . x and
A437: y in N and
Fn is continuous and
F | [:N, the carrier of I[01]:] = CircleMap * Fn and
A438: Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] and
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,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H by A274;
x in [:N, the carrier of I[01]:] by A435, A437, ZFMISC_1:87;
hence Ft . x = (Ft | [:N, the carrier of I[01]:]) . x by FUNCT_1:49
.= G . x by A7, A434, A436, A438, Lm14, FUNCT_1:49 ;
:: thesis:

end;

dom Ft = (dom G) /\ [: the carrier of Y,{0}:] by A8, A432, A430, XBOOLE_1:28;
hence G | [: the carrier of Y,{0}:] = Ft by A433, FUNCT_1:46; :: thesis:
let H be Function of [:Y,I[01]:],R^1; :: thesis:
assume that
A439: ( H is continuous & F = CircleMap * H ) and
A440: H | [: the carrier of Y,{0}:] = Ft ; :: thesis:
for x being Point of [:Y,I[01]:] holds G . x = H . x

proof

end;

hence G = H ; :: thesis: