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: for F being Function of [:Y,I[01]:],(Tunit_circle 2)

for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

let F be Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis: for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

let Ft be Function of [:Y,(Sspace 0[01]):],R^1; :: thesis: ( F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft implies ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) ) )

assume that

A3: F is continuous and

A4: Ft is continuous and

A5: F | [: the carrier of Y,{0}:] = CircleMap * Ft ; :: thesis: ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

defpred S_{1}[ 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_{1}[x,z]

A274: for x being Point of [:Y,I[01]:] holds S_{1}[x,G . x]
from FUNCT_2:sch 3(A9);

take G ; :: thesis: ( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

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]:]

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: for F being Function of [:Y,I[01]:],(Tunit_circle 2)

for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

let F be Function of [:Y,I[01]:],(Tunit_circle 2); :: thesis: for Ft being Function of [:Y,(Sspace 0[01]):],R^1 st F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft holds

ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

let Ft be Function of [:Y,(Sspace 0[01]):],R^1; :: thesis: ( F is continuous & Ft is continuous & F | [: the carrier of Y,{0}:] = CircleMap * Ft implies ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) ) )

assume that

A3: F is continuous and

A4: Ft is continuous and

A5: F | [: the carrier of Y,{0}:] = CircleMap * Ft ; :: thesis: ex G being Function of [:Y,I[01]:],R^1 st

( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft holds

G = H ) )

defpred S

( $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

proof

consider G being Function of [:Y,I[01]:],R^1 such that
let x be Point of [:Y,I[01]:]; :: thesis: ex z being Point of R^1 st S_{1}[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 (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_{2}[ 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;

_{2}[i] holds

S_{2}[i + 1]
_{2}[ 0 ]
by FINSEQ_3:24;

for i being Nat holds S_{2}[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: S_{1}[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,{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 ) )

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,{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 ) )

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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = Ft | [:N2, the carrier of I[01]:] ) by A10, A12, A179, A180, A182, A183, A184, A185, BORSUK_1:40; :: 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,{0}:] = 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,{0}:] = 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,{0}:] = Ft | [:N2, the carrier of I[01]:] ; :: thesis: Fn1 = H

defpred S_{3}[ 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_{3}[i] holds

S_{3}[i + 1]
_{3}[ 0 ]
by FINSEQ_3:24;

for i being Nat holds S_{3}[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: verum

end;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

( 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: 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) ) ) )

( 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 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: ( 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 A13, A20, A22, SEQM_3:def 1; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )

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: ( TT . i < 1 & 0 < TT . (i + 1) )

hence TT . i < 1 by A24, XXREAL_0:2; :: thesis: 0 < TT . (i + 1)

thus 0 < TT . (i + 1) by A13, A20, A21, A22, A23, SEQM_3:def 1; :: thesis: verum

end;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 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: ( 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 A13, A20, A22, SEQM_3:def 1; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )

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: ( TT . i < 1 & 0 < TT . (i + 1) )

hence TT . i < 1 by A24, XXREAL_0:2; :: thesis: 0 < TT . (i + 1)

thus 0 < TT . (i + 1) by A13, A20, A21, A22, A23, SEQM_3:def 1; :: thesis: verum

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]

A30:
for i being Nat st S[.(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

end;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 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: verum

end;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 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: verum

S

proof

A178:
S
let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume that

A31: S_{2}[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),(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]:] )

end;assume that

A31: S

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),(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]:] )

per cases
( i = 0 or i in dom TT )
by A32, TOPREALA:2;

end;

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),(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]:] )

( 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 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

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

.= [: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

end;( 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

proof

hence
F | [:N2,S:] = CircleMap * Fn
by A35, A37, A38; :: thesis: Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
let x be object ; :: thesis: ( x in dom (F | [:N2,S:]) implies (F | [:N2,S:]) . x = (CircleMap * Fn) . x )

assume A40: x in dom (F | [:N2,S:]) ; :: thesis: (F | [:N2,S:]) . x = (CircleMap * Fn) . x

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: verum

end;assume A40: x in dom (F | [:N2,S:]) ; :: thesis: (F | [:N2,S:]) . x = (CircleMap * Fn) . x

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: verum

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

dom (Ft | [:N2, the carrier of I[01]:]) =
[: the carrier of Y,{0}:] /\ [:N2, the carrier of I[01]:]
by A8, RELAT_1:61
A43:
[:N2,{0}:] c= [:N2, the carrier of I[01]:]
by Lm3, ZFMISC_1:95;

let x be object ; :: thesis: ( x in dom (Fn | [: the carrier of Y,{0}:]) implies (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x )

assume A44: x in dom (Fn | [: the carrier of Y,{0}:]) ; :: thesis: (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x

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: verum

end;let x be object ; :: thesis: ( x in dom (Fn | [: the carrier of Y,{0}:]) implies (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x )

assume A44: x in dom (Fn | [: the carrier of Y,{0}:]) ; :: thesis: (Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x

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: verum

.= [: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

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),(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]:] )

( 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 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

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 ")

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

Fn2 . p = Fni1 . p

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

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

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

end;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

proof

consider X1 being Subset of (Y | N2), Y1 being Subset of (I[01] | Ti) such that
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 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: verum

end;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 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: verum

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

then A102:
dom ((f ") * (F | [:N1,SS:])) = dom (F | [:N1,SS:])
by RELAT_1:27;
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 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: verum

end;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 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: verum

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

proof

A117:
Fn .: [:N1,{(TT . i)}:] c= Uit
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 A92, A93, XTUPLE_0:1; :: thesis: verum

end;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 A92, A93, XTUPLE_0:1; :: thesis: verum

proof

A121:
for p being set st p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds
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),(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: verum

end;assume b in Fn .: [:N1,{(TT . i)}:] ; :: thesis: b in Uit

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: verum

Fn2 . p = Fni1 . p

proof

A131:
[:N1,S:] c= [:N2,S:]
by A95, ZFMISC_1:96;
A122:
the carrier of (Y | N2) = N2
by PRE_TOPC:8;

let p be set ; :: thesis: ( p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p )

assume A123: p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; :: thesis: Fn2 . p = Fni1 . p

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: verum

end;let p be set ; :: thesis: ( p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p )

assume A123: p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) ; :: thesis: Fn2 . p = Fni1 . p

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: verum

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

proof

A162:
rng Fn1 c= dom CircleMap
by Lm12, TOPMETR:17;
let a be object ; :: thesis: ( a in dom (Fn1 | [: the carrier of Y,{0}:]) implies (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a )

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: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a

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;

end;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: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a

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
( not a in dom Fni1 or a in dom Fni1 )
;

end;

suppose A153:
not a in dom Fni1
; :: thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a

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: verum

end;.= (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: verum

suppose A154:
a in dom Fni1
; :: thesis: (Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a

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: verum

end;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: verum

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

A173:
S c= S1
by XBOOLE_1:7;
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

end;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 )
;

end;

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 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: verum

end;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: verum

suppose A171:
not a in dom Fni1
; :: thesis: (CircleMap * Fn1) . a = F . a

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: verum

end;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: verum

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

for i being Nat holds S

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: S

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,{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 ) )

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,{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 ) )

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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = 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,{0}:] = Ft | [:N2, the carrier of I[01]:] ) by A10, A12, A179, A180, A182, A183, A184, A185, BORSUK_1:40; :: 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,{0}:] = 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,{0}:] = 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,{0}:] = Ft | [:N2, the carrier of I[01]:] ; :: thesis: Fn1 = H

defpred S

( 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

S

proof

A271:
S
let i be Nat; :: thesis: ( S_{3}[i] implies S_{3}[i + 1] )

assume that

A193: S_{3}[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:] )

end;assume that

A193: S

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 A194, TOPREALA:2;

end;

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:] )

( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )

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

thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:N2,Z:] = H | [:N2,Z:]

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: verum

end;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

take
Z
; :: thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )
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 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: verum

end;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 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: verum

thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:N2,Z:] = H | [:N2,Z:]

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: verum

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:] )

( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )

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: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] )

A207: TT . i < TT . (i + 1) by A19, A194, A202;

hence Z1 = [.0,(TT . (i + 1)).] by A205, A203, XXREAL_1:165; :: 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 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

hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by A189, A210, RELAT_1:62; :: thesis: verum

end;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: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] )

A207: TT . i < TT . (i + 1) by A19, A194, A202;

hence Z1 = [.0,(TT . (i + 1)).] by A205, A203, XXREAL_1:165; :: 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 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

dom (H | [:N2,Z1:]) = [:N2,Z1:]
by A191, A190, A208, RELAT_1:62;
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: ( 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 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

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

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

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

A263: for x being object st x in dom (f * (Fn1 | [:xy,ZZ:])) holds

(f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x

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;

end;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: ( 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 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

A230:
D is Cover of H .: xZZ
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 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: verum

end;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 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: verum

proof

A235:
H . [x1,(TT . i)] in REAL
by XREAL_0:def 1;
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) = (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: verum

end;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) = (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: verum

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

( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit )
by PRE_TOPC:8;
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 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: verum

end;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 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: verum

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

Fn1 . [x1,(TT . i)] in Fn1 .: xZZ
by A247, FUNCT_2:35;
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 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: verum

end;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 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: verum

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

then A262:
dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:])
by RELAT_1:27;
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 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: verum

end;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 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: verum

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

f is being_homeomorphism
by A216, A243;
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 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: verum

end;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 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: verum

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
( x2 in ZZ or not x2 in ZZ )
;

end;

suppose
x2 in ZZ
; :: thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x

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: verum

end;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: verum

suppose
not x2 in ZZ
; :: thesis: (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x

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: verum

end;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: verum

hence Fn1 | [:N2,Z1:] = H | [:N2,Z1:] by A189, A210, RELAT_1:62; :: thesis: verum

for i being Nat holds S

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: verum

A274: for x being Point of [:Y,I[01]:] holds S

take G ; :: thesis: ( G is continuous & F = CircleMap * G & G | [: the carrier of Y,{0}:] = Ft & ( for H being Function of [:Y,I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = 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]:]

A276:
for p being Point of [:Y,I[01]:]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;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

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: 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]:]

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,{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]:]

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,{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]:]

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,{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]:]

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,{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]:]

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,{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]:] 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,{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: Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

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_{2}[ 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_{2}[i] holds

S_{2}[i + 1]

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]:]

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,{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]:]

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,{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]:]

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,{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]:]

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,{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]:]

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,{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]:] 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,{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: Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]

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

( 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

S

proof

let i be Nat; :: thesis: ( S_{2}[i] implies S_{2}[i + 1] )

assume that

A302: S_{2}[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:] )

assume that

A302: S

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 A303, TOPREALA:2;

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:] )

( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )

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

thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]

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: verum

end;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

take
Z
; :: thesis: ( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
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 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: verum

end;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 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: verum

thus Z = [.0,(TT . (i + 1)).] ; :: thesis: Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]

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: verum

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:] )

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;

take Z1 = Z \/ ZZ; :: thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] )

A327: TT . i < TT . (i + 1) by A303, A312, A313;

hence Z1 = [.0,(TT . (i + 1)).] by A321, A319, XXREAL_1:165; :: thesis: Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]

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

( 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) ) ) )

then A319:
0 <= TT . i
by A312;( 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 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: ( 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 A288, A314, A316, SEQM_3:def 1; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )

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: ( TT . i < 1 & 0 < TT . (i + 1) )

hence TT . i < 1 by A318, XXREAL_0:2; :: thesis: 0 < TT . (i + 1)

thus 0 < TT . (i + 1) by A288, A314, A315, A316, A317, SEQM_3:def 1; :: thesis: verum

end;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 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: ( 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 A288, A314, A316, SEQM_3:def 1; :: thesis: ( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )

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: ( TT . i < 1 & 0 < TT . (i + 1) )

hence TT . i < 1 by A318, XXREAL_0:2; :: thesis: 0 < TT . (i + 1)

thus 0 < TT . (i + 1) by A288, A314, A315, A316, A317, SEQM_3:def 1; :: thesis: verum

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: for i being Nat st 0 <= TT . i & TT . (i + 1) <= 1 holds

[.(TT . i),(TT . (i + 1)).] c= the carrier of I[01]

then reconsider ZZ = [.(TT . i),(TT . (i + 1)).] as Subset of I[01] by A319, A320;[.(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

end;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 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: verum

end;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 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: verum

take Z1 = Z \/ ZZ; :: thesis: ( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] )

A327: TT . i < TT . (i + 1) by A303, A312, A313;

hence Z1 = [.0,(TT . (i + 1)).] by A321, A319, XXREAL_1:165; :: thesis: Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]

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: ( 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 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

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

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

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

[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

A394: rng (Fn2 | [:xy,ZZ:]) c= dom f

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 ;

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: ( 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 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

A353:
I[01] is SubSpace of I[01]
by TSEP_1:2;
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 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: verum

end;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 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: verum

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

A361:
TT . i in Z
by A321, A319, XXREAL_1:1;
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 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: verum

end;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 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: verum

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

( the carrier of ((Tunit_circle 2) | Ui) = Ui & the carrier of (R^1 | Uit) = Uit )
by PRE_TOPC:8;
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 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: verum

end;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 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: verum

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

then A383:
dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:])
by RELAT_1:27;
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 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: verum

end;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 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: verum

[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

A393:
dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:]
by A293, A297, A341, RELAT_1:62, ZFMISC_1:96;
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 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: verum

end;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 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: verum

A394: rng (Fn2 | [:xy,ZZ:]) c= dom f

proof

then
dom (f * (Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:])
by RELAT_1:27;
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 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: verum

end;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 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: verum

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
( 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 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: verum

end;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: verum