take N2 = N; :: thesis: 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 . (i + 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]:] )
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;
( 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: ex Fn being Function of [:(Y | N2),(I[01] | S):],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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = Ft | [:N2, the carrier of I[01]:] )
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: ( F | [:N2,S:] = CircleMap * Fn & Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] )
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 hence F | [:N2,S:] = CircleMap * Fn by A35, A37, A38; :: thesis: Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
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 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: verum

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, TOPMETR:17;
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;
then reconsider FnT = Fn | [:N2,Ti:] as Function of [:(Y | N2),(I[01] | Ti):],R^1 by A67, A68, A65, 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 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 ") 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 ;
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 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;
set Fn1 = (Fn | [:N1,S:]) +* Fni1;
reconsider Fn2 = Fn | [:N1,S:] as Function of [:(Y | N1),(I[01] | S):],R^1 by A105, A108, FUNCT_2:2;
A112: rng ((Fn | [:N1,S:]) +* Fni1) c= (rng (Fn | [:N1,S:])) \/ (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 ((Fn | [:N1,S:]) +* 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 A117: Fn .: [:N1,{(TT . i)}:] c= Uit A121: for p being set st p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds
Fn2 . p = Fni1 . p 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: ex S being non empty Subset of I[01] ex Fn being Function of [:(Y | N1),(I[01] | S):],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,{0}:] = 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,{0}:] = 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 A103, BORSUK_1:def 2;
then reconsider Fn1 = (Fn | [:N1,S:]) +* Fni1 as Function of [:(Y | N1),(I[01] | S1):],R^1 by A136, A113, A112, FUNCT_2:2, XBOOLE_1:1;
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,{0}:] = Ft | [:N1, the carrier of I[01]:] )
thus A138: S1 = [.0,(TT . (i + 1)).] by A54, A62, A52, XXREAL_1:165; :: thesis: ( y in N1 & N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
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 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 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: ( N1 c= N & Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
thus N1 c= N by A56, A95; :: thesis: ( Fn1 is continuous & F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
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: ( F | [:N1,S1:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] )
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: Fn1 | [: the carrier of Y,{0}:] = 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),({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: verum