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; 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); 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; ( 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
; 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 S1[ set , set ] means ex y being Point of Y ex t being Point of I[01] ex N being non empty open Subset of Y ex Fn being Function of [:(Y | N),I[01]:],R^1 st
( $1 = [y,t] & $2 = Fn . $1 & y in N & Fn is continuous & F | [:N, the carrier of I[01]:] = CircleMap * Fn & Fn | [: the carrier of Y,{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 5
;
A7:
the carrier of [:Y,(Sspace 0[01]):] = [: the carrier of Y, the carrier of (Sspace 0[01]):]
by BORSUK_1:def 5;
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 S1[x,z]
proof
let x be
Point of
[:Y,I[01]:];
ex z being Point of R^1 st S1[x,z]
consider y being
Point of
Y,
t being
Point of
I[01] such that A10:
x = [y,t]
by BORSUK_1:50;
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
natural number 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
natural number 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 S2[
Element of
NAT ]
means ( $1
in dom TT implies ex
N2 being non
empty open Subset of
Y ex
S being non
empty Subset of
I[01] ex
Fn being
Function of
[:(Y | N2),(I[01] | S):],
R^1 st
(
S = [.0,(TT . $1).] &
y in N2 &
N2 c= N &
Fn is
continuous &
F | [:N2,S:] = CircleMap * Fn &
Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] ) );
A17:
len TT in dom TT
by FINSEQ_5:6;
A18:
1
in dom TT
by FINSEQ_5:6;
A19:
now let i be
Element of
NAT ;
( 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
;
( 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:27;
then
( 1
= i or 1
< i )
by XXREAL_0:1;
hence A21:
0 <= TT . i
by A11, A13, A18, A20, SEQM_3:def 1;
( 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
;
( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )A23:
i + 0 < i + 1
by XREAL_1:10;
hence A24:
TT . i < TT . (i + 1)
by A13, A20, A22, SEQM_3:def 1;
( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
i + 1
<= len TT
by A22, FINSEQ_3:27;
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;
( TT . i < 1 & 0 < TT . (i + 1) )hence
TT . i < 1
by A24, XXREAL_0:2;
0 < TT . (i + 1)thus
0 < TT . (i + 1)
by A13, A20, A21, A22, A23, SEQM_3:def 1;
verum end;
A30:
for
i being
Element of
NAT st
S2[
i] holds
S2[
i + 1]
proof
let i be
Element of
NAT ;
( S2[i] implies S2[i + 1] )
assume that A31:
S2[
i]
and A32:
i + 1
in dom TT
;
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:23;
suppose A33:
i = 0
;
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]:] )take N2 =
N;
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:91, ZFMISC_1:119;
reconsider K0 =
[:N2,S:] as non
empty Subset of
[:Y,(Sspace 0[01]):] by A7, A34, Lm14, ZFMISC_1:119;
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 5;
( the
carrier of
(Y | N2) = N2 & the
carrier of
(I[01] | S) = S )
by PRE_TOPC:29;
then reconsider Fn =
Ft | [:N2,{0}:] as
Function of
[:(Y | N2),(I[01] | S):],
R^1 by A35, A36, FUNCT_2:4;
A37:
dom (F | [:N2,S:]) = [:N2,S:]
by A6, RELAT_1:91, ZFMISC_1:119;
reconsider S1 =
S as non
empty Subset of
(Sspace 0[01]) by A11, A33, Lm14, XXREAL_1:17;
take
S
;
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
;
( 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)).]
;
( 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;
( 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
;
( 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:6
.=
(Sspace 0[01]) | S1
by A34, Lm14, TSEP_1:3
;
then
[:(Y | N2),(I[01] | S):] = [:Y,(Sspace 0[01]):] | K0
by BORSUK_3:26;
hence
Fn is
continuous
by A4, A34, TOPMETR:10;
( 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:24;
then A38:
dom (CircleMap * Fn) = dom Fn
by RELAT_1:46;
A39:
[:N2,S:] c= dom Ft
by A8, A34, ZFMISC_1:119;
for
x being
set st
x in dom (F | [:N2,S:]) holds
(F | [:N2,S:]) . x = (CircleMap * Fn) . x
proof
let x be
set ;
( x in dom (F | [:N2,S:]) implies (F | [:N2,S:]) . x = (CircleMap * Fn) . x )
assume A40:
x in dom (F | [:N2,S:])
;
(F | [:N2,S:]) . x = (CircleMap * Fn) . x
thus (F | [:N2,S:]) . x =
F . x
by A37, A40, FUNCT_1:72
.=
(CircleMap * Ft) . x
by A5, A7, A35, A37, A40, Lm14, FUNCT_1:72
.=
CircleMap . (Ft . x)
by A39, A37, A40, FUNCT_1:23
.=
CircleMap . (Fn . x)
by A34, A37, A40, FUNCT_1:72
.=
(CircleMap * Fn) . x
by A35, A37, A40, FUNCT_1:23
;
verum
end; hence
F | [:N2,S:] = CircleMap * Fn
by A35, A37, A38, FUNCT_1:9;
Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]A41:
dom (Fn | [: the carrier of Y,{0}:]) = [:N2,S:] /\ [: the carrier of Y,{0}:]
by A35, RELAT_1:90;
A42:
for
x being
set st
x in dom (Fn | [: the carrier of Y,{0}:]) holds
(Fn | [: the carrier of Y,{0}:]) . x = (Ft | [:N2, the carrier of I[01]:]) . x
proof
A43:
[:N2,{0}:] c= [:N2, the carrier of I[01]:]
by Lm3, ZFMISC_1:118;
let x be
set ;
( 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}:])
;
(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:72
.=
Ft . x
by A45, FUNCT_1:72
.=
(Ft | [:N2, the carrier of I[01]:]) . x
by A45, A43, FUNCT_1:72
;
verum
end; dom (Ft | [:N2, the carrier of I[01]:]) =
[: the carrier of Y,{0}:] /\ [:N2, the carrier of I[01]:]
by A8, RELAT_1:90
.=
[:N2,S:]
by A34, ZFMISC_1:124
;
hence
Fn | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
by A34, A41, A42, FUNCT_1:9, ZFMISC_1:124;
verum end; suppose A46:
i in dom TT
;
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]:] )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:29;
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:106;
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 5;
N2 c= N2
;
then reconsider N7 =
N2 as non
empty Subset of
(Y | N2) by PRE_TOPC:29;
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:37;
A64:
the
carrier of
(I[01] | S) = S
by PRE_TOPC:29;
then reconsider Ti2 =
Ti as non
empty Subset of
(I[01] | S) by A63, ZFMISC_1:37;
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 5, TOPMETR:24;
A66:
[:N2,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:]
by A56, ZFMISC_1:119;
A67:
the
carrier of
(Y | N2) = N2
by PRE_TOPC:29;
{(TT . i)} c= S
by A63, ZFMISC_1:37;
then A68:
dom (Fn | [:N2,Ti:]) = [:N2,{(TT . i)}:]
by A64, A60, A67, A61, RELAT_1:91, ZFMISC_1:119;
A69:
[:((Y | N2) | N7),((I[01] | S) | Ti2):] = [:(Y | N2),(I[01] | S):] | [:N7,Ti2:]
by BORSUK_3:26;
A70:
the
carrier of
(I[01] | Ti) = Ti
by PRE_TOPC:29;
then reconsider FnT =
Fn | [:N2,Ti:] as
Function of
[:(Y | N2),(I[01] | Ti):],
R^1 by A67, A68, A65, FUNCT_2:4;
(
(Y | N2) | N7 = Y | N2 &
(I[01] | S) | Ti2 = I[01] | Ti )
by GOBOARD9:4;
then A71:
FnT is
continuous
by A57, A69, TOPMETR:10;
[y,(TT . i)] in dom F
by A6, A63, ZFMISC_1:106;
then A72:
F . [y,(TT . i)] in F .: [:N,[.(TT . i),(TT . (i + 1)).]:]
by A53, FUNCT_2:43;
A73:
[y,(TT . i)] in [:N2,S:]
by A55, A63, ZFMISC_1:106;
then F . [y,(TT . i)] =
(CircleMap * Fn) . [y,(TT . i)]
by A58, FUNCT_1:72
.=
CircleMap . (Fn . [y,(TT . i)])
by A64, A60, A67, A73, FUNCT_2:21
;
then
Fn . [y,(TT . i)] in CircleMap " Ui
by A48, A72, FUNCT_2:46, TOPMETR:24;
then consider Uit being
set such that A74:
Fn . [y,(TT . i)] in Uit
and A75:
Uit in D
by A49, TARSKI:def 4;
reconsider Uit =
Uit as non
empty Subset of
R^1 by A74, A75;
(
[#] R^1 <> {} &
Uit is
open )
by A75, TOPS_2:def 1;
then
FnT " Uit is
open
by A71, TOPS_2:55;
then consider SF being
Subset-Family of
[:(Y | N2),(I[01] | Ti):] such that A76:
FnT " Uit = union SF
and A77:
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:45;
A78:
TT . i in {(TT . i)}
by TARSKI:def 1;
then A79:
[y,(TT . i)] in [:N2,{(TT . i)}:]
by A55, ZFMISC_1:def 2;
then
FnT . [y,(TT . i)] in Uit
by A74, FUNCT_1:72;
then
[y,(TT . i)] in FnT " Uit
by A79, A68, FUNCT_1:def 13;
then consider N5 being
set such that A80:
[y,(TT . i)] in N5
and A81:
N5 in SF
by A76, TARSKI:def 4;
set f =
CircleMap | Uit;
A82:
dom (CircleMap | Uit) = Uit
by Lm12, RELAT_1:91, TOPMETR:24;
A83:
rng (CircleMap | Uit) c= Ui
consider X1 being
Subset of
(Y | N2),
Y1 being
Subset of
(I[01] | Ti) such that A86:
N5 = [:X1,Y1:]
and A87:
X1 is
open
and
Y1 is
open
by A77, A81;
the
carrier of
(R^1 | Uit) = Uit
by PRE_TOPC:29;
then reconsider f =
CircleMap | Uit as
Function of
(R^1 | Uit),
((Tunit_circle 2) | Ui) by A51, A82, A83, FUNCT_2:4;
consider NY being
Subset of
Y such that A88:
NY is
open
and A89:
NY /\ ([#] (Y | N2)) = X1
by A87, TOPS_2:32;
consider y1,
y2 being
set such that A90:
y1 in X1
and A91:
y2 in Y1
and A92:
[y,(TT . i)] = [y1,y2]
by A80, A86, ZFMISC_1:def 2;
set N1 =
NY /\ N2;
y = y1
by A92, ZFMISC_1:33;
then A93:
y in NY
by A89, A90, XBOOLE_0:def 4;
then reconsider N1 =
NY /\ N2 as non
empty open Subset of
Y by A55, A88, XBOOLE_0:def 4;
A94:
N1 c= N2
by XBOOLE_1:17;
then
[:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N2,[.(TT . i),(TT . (i + 1)).]:]
by ZFMISC_1:119;
then
[:N1,[.(TT . i),(TT . (i + 1)).]:] c= [:N,[.(TT . i),(TT . (i + 1)).]:]
by A66, XBOOLE_1:1;
then A95:
F .: [:N1,[.(TT . i),(TT . (i + 1)).]:] c= F .: [:N,[.(TT . i),(TT . (i + 1)).]:]
by RELAT_1:156;
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;
A96:
dom (F | [:N1,SS:]) = [:N1,SS:]
by A6, RELAT_1:91, ZFMISC_1:119;
set Fni1 =
(f ") * (F | [:N1,SS:]);
f " is
being_homeomorphism
by A50, A75, TOPS_2:70;
then A97:
dom (f ") = [#] ((Tunit_circle 2) | Ui)
by TOPS_2:def 5;
A98:
rng (F | [:N1,SS:]) c= dom (f ")
proof
let b be
set ;
TARSKI:def 3 ( not b in rng (F | [:N1,SS:]) or b in dom (f ") )
assume
b in rng (F | [:N1,SS:])
;
b in dom (f ")
then consider a being
set such that A99:
a in dom (F | [:N1,SS:])
and A100:
(F | [:N1,SS:]) . a = b
by FUNCT_1:def 5;
b = F . a
by A96, A99, A100, FUNCT_1:72;
then
b in F .: [:N1,SS:]
by A96, A99, FUNCT_2:43;
then
b in F .: [:N,SS:]
by A95;
then
b in Ui
by A48;
hence
b in dom (f ")
by A97, PRE_TOPC:29;
verum
end; then A101:
dom ((f ") * (F | [:N1,SS:])) = dom (F | [:N1,SS:])
by RELAT_1:46;
set Fn2 =
Fn | [:N1,S:];
A102:
the
carrier of
(Y | N1) = N1
by PRE_TOPC:29;
then A103:
[:N1,S:] = the
carrier of
[:(Y | N1),(I[01] | S):]
by A64, BORSUK_1:def 5;
then A104:
dom (Fn | [:N1,S:]) = the
carrier of
[:(Y | N1),(I[01] | S):]
by A64, A60, A67, A61, A94, RELAT_1:91, ZFMISC_1:119;
reconsider ff =
f as
Function ;
A105:
f is
being_homeomorphism
by A50, A75;
then A106:
f is
one-to-one
by TOPS_2:def 5;
A107:
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 A108:
rng ((f ") * (F | [:N1,SS:])) c= the
carrier of
R^1
by XBOOLE_1:1;
A109:
the
carrier of
(I[01] | SS) = SS
by PRE_TOPC:29;
then A110:
[:N1,SS:] = the
carrier of
[:(Y | N1),(I[01] | SS):]
by A102, BORSUK_1:def 5;
then reconsider Fni1 =
(f ") * (F | [:N1,SS:]) as
Function of
[:(Y | N1),(I[01] | SS):],
R^1 by A96, A101, A108, FUNCT_2:4;
set Fn1 =
(Fn | [:N1,S:]) +* Fni1;
reconsider Fn2 =
Fn | [:N1,S:] as
Function of
[:(Y | N1),(I[01] | S):],
R^1 by A104, A107, FUNCT_2:4;
A111:
rng ((Fn | [:N1,S:]) +* Fni1) c= (rng (Fn | [:N1,S:])) \/ (rng Fni1)
by FUNCT_4:18;
dom (Fn | [:N1,S:]) = [:N1,S:]
by A64, A60, A67, A61, A94, RELAT_1:91, ZFMISC_1:119;
then A112:
dom ((Fn | [:N1,S:]) +* Fni1) = [:N1,S:] \/ [:N1,SS:]
by A96, A101, FUNCT_4:def 1;
A113:
rng f = [#] ((Tunit_circle 2) | Ui)
by A105, TOPS_2:def 5;
then A114:
f " = ff "
by A106, TOPS_2:def 4;
A115:
Y1 = Ti
A116:
Fn .: [:N1,{(TT . i)}:] c= Uit
proof
let b be
set ;
TARSKI:def 3 ( not b in Fn .: [:N1,{(TT . i)}:] or b in Uit )
assume
b in Fn .: [:N1,{(TT . i)}:]
;
b in Uit
then consider a being
Point of
[:(Y | N2),(I[01] | S):] such that A117:
a in [:N1,{(TT . i)}:]
and A118:
Fn . a = b
by FUNCT_2:116;
a in N5
by A86, A89, A115, A117, PRE_TOPC:def 10;
then A119:
a in union SF
by A81, TARSKI:def 4;
then
a in dom FnT
by A76, FUNCT_1:def 13;
then
Fn . a = FnT . a
by FUNCT_1:70;
hence
b in Uit
by A76, A118, A119, FUNCT_1:def 13;
verum
end; A120:
for
p being
set st
p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) holds
Fn2 . p = Fni1 . p
proof
A121:
the
carrier of
(Y | N2) = N2
by PRE_TOPC:29;
let p be
set ;
( p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):]) implies Fn2 . p = Fni1 . p )
assume A122:
p in ([#] [:(Y | N1),(I[01] | S):]) /\ ([#] [:(Y | N1),(I[01] | SS):])
;
Fn2 . p = Fni1 . p
A123:
p in ([#] [:(Y | N1),(I[01] | SS):]) /\ ([#] [:(Y | N1),(I[01] | S):])
by A122;
then A124:
Fn . p = Fn2 . p
by A103, FUNCT_1:72;
[:N1,S:] /\ [:N1,SS:] = [:N1,(S /\ SS):]
by ZFMISC_1:122;
then A125:
p in [:N1,{(TT . i)}:]
by A54, A62, A52, A110, A103, A122, XXREAL_1:418;
then consider p1 being
Element of
N1,
p2 being
Element of
{(TT . i)} such that A126:
p = [p1,p2]
by DOMAIN_1:9;
A127:
p1 in N1
;
S /\ SS = {(TT . i)}
by A54, A62, A52, XXREAL_1:418;
then
p2 in S
by XBOOLE_0:def 4;
then A128:
p in [:N2,S:]
by A94, A126, A127, ZFMISC_1:def 2;
then A129:
Fn . p in Fn .: [:N1,{(TT . i)}:]
by A64, A60, A67, A125, FUNCT_2:43;
(F | [:N1,SS:]) . p =
F . p
by A110, A122, FUNCT_1:72
.=
(F | [:N2,S:]) . p
by A128, FUNCT_1:72
.=
CircleMap . (Fn . p)
by A58, A64, A60, A61, A121, A128, FUNCT_1:23
.=
(CircleMap | Uit) . (Fn . p)
by A116, A129, FUNCT_1:72
.=
ff . (Fn2 . p)
by A103, A123, FUNCT_1:72
;
hence Fn2 . p =
(ff ") . ((F | [:N1,SS:]) . p)
by A116, A82, A106, A124, A129, FUNCT_1:54
.=
Fni1 . p
by A114, A96, A110, A122, FUNCT_1:23
;
verum
end; A130:
[:N1,S:] c= [:N2,S:]
by A94, ZFMISC_1:119;
then reconsider K0 =
[:N1,S:] as
Subset of
[:(Y | N2),(I[01] | S):] by A64, A60, PRE_TOPC:29;
A131:
[:N1,SS:] c= dom F
by A6, ZFMISC_1:119;
reconsider gF =
F | [:N1,SS:] as
Function of
[:(Y | N1),(I[01] | SS):],
(Tunit_circle 2) by A96, A98, A110, FUNCT_2:4;
reconsider fF =
F | [:N1,SS:] as
Function of
[:(Y | N1),(I[01] | SS):],
((Tunit_circle 2) | Ui) by A97, A96, A98, A110, FUNCT_2:4;
[:(Y | N1),(I[01] | SS):] = [:Y,I[01]:] | [:N1,SS:]
by BORSUK_3:26;
then
gF is
continuous
by A3, TOPMETR:10;
then A132:
fF is
continuous
by TOPMETR:9;
f " is
continuous
by A105, TOPS_2:def 5;
then
(f ") * fF is
continuous
by A132;
then A133:
Fni1 is
continuous
by PRE_TOPC:56;
reconsider aN1 =
N1 as non
empty Subset of
(Y | N2) by A94, PRE_TOPC:29;
S c= S
;
then reconsider aS =
S as non
empty Subset of
(I[01] | S) by PRE_TOPC:29;
[:(Y | N2),(I[01] | S):] | K0 =
[:((Y | N2) | aN1),((I[01] | S) | aS):]
by BORSUK_3:26
.=
[:(Y | N1),((I[01] | S) | aS):]
by GOBOARD9:4
.=
[:(Y | N1),(I[01] | S):]
by GOBOARD9:4
;
then A134:
Fn2 is
continuous
by A57, TOPMETR:10;
take
N1
;
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;
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]:] )A135:
[:N1,S:] \/ [:N1,SS:] = [:N1,S1:]
by ZFMISC_1:120;
A136:
the
carrier of
(I[01] | S1) = S1
by PRE_TOPC:29;
then
[:N1,S1:] = the
carrier of
[:(Y | N1),(I[01] | S1):]
by A102, BORSUK_1:def 5;
then reconsider Fn1 =
(Fn | [:N1,S:]) +* Fni1 as
Function of
[:(Y | N1),(I[01] | S1):],
R^1 by A135, A112, A111, FUNCT_2:4, XBOOLE_1:1;
take
Fn1
;
( 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 A137:
S1 = [.0,(TT . (i + 1)).]
by A54, A62, A52, XXREAL_1:165;
( 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 A137, XXREAL_1:1;
then A138:
{0} c= S1
by ZFMISC_1:37;
A139:
dom (Fn1 | [: the carrier of Y,{0}:]) = (dom Fn1) /\ [: the carrier of Y,{0}:]
by RELAT_1:90;
then A140:
dom (Fn1 | [: the carrier of Y,{0}:]) =
[:(N1 /\ the carrier of Y),(S1 /\ {0}):]
by A135, A112, ZFMISC_1:123
.=
[:N1,(S1 /\ {0}):]
by XBOOLE_1:28
.=
[:N1,{0}:]
by A138, XBOOLE_1:28
;
A141:
for
a being
set st
a in dom (Fn1 | [: the carrier of Y,{0}:]) holds
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
proof
let a be
set ;
( 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 )
A142:
[:N1, the carrier of I[01]:] c= [:N2, the carrier of I[01]:]
by A94, ZFMISC_1:119;
assume A143:
a in dom (Fn1 | [: the carrier of Y,{0}:])
;
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . a
then A144:
a in [: the carrier of Y,{0}:]
by A139, XBOOLE_0:def 4;
then consider a1,
a2 being
set such that
a1 in the
carrier of
Y
and A145:
a2 in {0}
and A146:
a = [a1,a2]
by ZFMISC_1:def 2;
A147:
a2 = 0
by A145, TARSKI:def 1;
0 in S
by A54, A62, XXREAL_1:1;
then
{0} c= S
by ZFMISC_1:37;
then A148:
[:N1,{0}:] c= [:N1,S:]
by ZFMISC_1:119;
then A149:
a in [:N1,S:]
by A140, A143;
A150:
[:N1,S:] c= [:N1, the carrier of I[01]:]
by ZFMISC_1:119;
then A151:
a in [:N1, the carrier of I[01]:]
by A149;
per cases
( not a in dom Fni1 or a in dom Fni1 )
;
suppose A152:
not
a in dom Fni1
;
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . athus (Fn1 | [: the carrier of Y,{0}:]) . a =
Fn1 . a
by A144, FUNCT_1:72
.=
(Fn | [:N1,S:]) . a
by A152, FUNCT_4:12
.=
Fn . a
by A140, A143, A148, FUNCT_1:72
.=
(Ft | [:N2, the carrier of I[01]:]) . a
by A59, A144, FUNCT_1:72
.=
Ft . a
by A151, A142, FUNCT_1:72
.=
(Ft | [:N1, the carrier of I[01]:]) . a
by A149, A150, FUNCT_1:72
;
verum end; suppose A153:
a in dom Fni1
;
(Fn1 | [: the carrier of Y,{0}:]) . a = (Ft | [:N1, the carrier of I[01]:]) . aset e =
(Ft | [:N1, the carrier of I[01]:]) . a;
a in [:N1,SS:]
by A6, A101, A153, RELAT_1:91, ZFMISC_1:119;
then consider b1,
b2 being
set such that A154:
b1 in N1
and A155:
b2 in SS
and A156:
a = [b1,b2]
by ZFMISC_1:def 2;
a2 = b2
by A146, A156, ZFMISC_1:33;
then A157:
a2 = TT . i
by A62, A147, A155, XXREAL_1:1;
a1 = b1
by A146, A156, ZFMISC_1:33;
then A158:
(
[a1,(TT . i)] in [:N1,S:] &
[a1,(TT . i)] in [:N1,{(TT . i)}:] )
by A63, A78, A154, ZFMISC_1:106;
(Ft | [:N1, the carrier of I[01]:]) . a =
Ft . a
by A149, A150, FUNCT_1:72
.=
(Ft | [:N2, the carrier of I[01]:]) . a
by A151, A142, FUNCT_1:72
.=
Fn . a
by A59, A144, FUNCT_1:72
;
then A159:
(Ft | [:N1, the carrier of I[01]:]) . a in Fn .: [:N1,{(TT . i)}:]
by A64, A60, A67, A61, A130, A146, A157, A158, FUNCT_1:def 12;
then A160:
ff . ((Ft | [:N1, the carrier of I[01]:]) . a) =
CircleMap . ((Ft | [:N1, the carrier of I[01]:]) . a)
by A116, FUNCT_1:72
.=
CircleMap . (Ft . a)
by A149, A150, FUNCT_1:72
.=
(CircleMap * Ft) . a
by A8, A144, FUNCT_1:23
.=
F . a
by A5, A144, FUNCT_1:72
;
thus (Fn1 | [: the carrier of Y,{0}:]) . a =
Fn1 . a
by A144, FUNCT_1:72
.=
Fni1 . a
by A153, FUNCT_4:14
.=
(ff ") . ((F | [:N1,SS:]) . a)
by A114, A101, A153, FUNCT_1:23
.=
(ff ") . (F . a)
by A96, A101, A153, FUNCT_1:72
.=
(Ft | [:N1, the carrier of I[01]:]) . a
by A116, A82, A106, A159, A160, FUNCT_1:54
;
verum end;
end; A161:
rng Fn1 c= dom CircleMap
by Lm12, TOPMETR:24;
then A162:
dom (CircleMap * Fn1) = dom Fn1
by RELAT_1:46;
A163:
for
a being
set st
a in dom (CircleMap * Fn1) holds
(CircleMap * Fn1) . a = F . a
proof
let a be
set ;
( a in dom (CircleMap * Fn1) implies (CircleMap * Fn1) . a = F . a )
assume A164:
a in dom (CircleMap * Fn1)
;
(CircleMap * Fn1) . a = F . a
per cases
( a in dom Fni1 or not a in dom Fni1 )
;
suppose A165:
a in dom Fni1
;
(CircleMap * Fn1) . a = F . aA166:
[:N1,SS:] c= [: the carrier of Y, the carrier of I[01]:]
by ZFMISC_1:119;
A167:
a in [:N1,SS:]
by A6, A101, A165, RELAT_1:91, ZFMISC_1:119;
then
F . a in F .: [:N1,SS:]
by A6, A166, FUNCT_1:def 12;
then A168:
F . a in F .: [:N,SS:]
by A95;
then
a in F " (dom (ff "))
by A6, A48, A51, A97, A114, A167, A166, FUNCT_1:def 13;
then A169:
a in dom ((ff ") * F)
by RELAT_1:182;
thus (CircleMap * Fn1) . a =
CircleMap . (Fn1 . a)
by A164, FUNCT_2:21
.=
CircleMap . (Fni1 . a)
by A165, FUNCT_4:14
.=
CircleMap . ((f ") . ((F | [:N1,SS:]) . a))
by A101, A165, FUNCT_1:23
.=
CircleMap . ((f ") . (F . a))
by A96, A101, A165, FUNCT_1:72
.=
CircleMap . (((ff ") * F) . a)
by A131, A114, A96, A101, A165, FUNCT_1:23
.=
(CircleMap * ((ff ") * F)) . a
by A169, FUNCT_1:23
.=
((CircleMap * (ff ")) * F) . a
by RELAT_1:55
.=
(CircleMap * (ff ")) . (F . a)
by A131, A96, A101, A165, FUNCT_1:23
.=
F . a
by A48, A51, A113, A106, A168, TOPALG_3:2
;
verum end; suppose A170:
not
a in dom Fni1
;
(CircleMap * Fn1) . a = F . athen A171:
a in [:N1,S:]
by A96, A101, A112, A162, A164, XBOOLE_0:def 3;
thus (CircleMap * Fn1) . a =
CircleMap . (Fn1 . a)
by A164, FUNCT_2:21
.=
CircleMap . ((Fn | [:N1,S:]) . a)
by A170, FUNCT_4:12
.=
CircleMap . (Fn . a)
by A171, FUNCT_1:72
.=
(CircleMap * Fn) . a
by A64, A60, A67, A130, A171, FUNCT_2:21
.=
F . a
by A58, A130, A171, FUNCT_1:72
;
verum end;
end; A172:
S c= S1
by XBOOLE_1:7;
then A173:
(
[#] (I[01] | S1) = the
carrier of
(I[01] | S1) &
I[01] | S is
SubSpace of
I[01] | S1 )
by A64, A136, TSEP_1:4;
A174:
SS c= S1
by XBOOLE_1:7;
then reconsider F1 =
[#] (I[01] | S),
F2 =
[#] (I[01] | SS) as
Subset of
(I[01] | S1) by A136, A172, PRE_TOPC:29;
reconsider hS =
F1,
hSS =
F2 as
Subset of
I[01] by PRE_TOPC:29;
hS is
closed
by A54, BORSUK_4:48, PRE_TOPC:29;
then A175:
F1 is
closed
by TSEP_1:8;
thus
y in N1
by A55, A93, XBOOLE_0:def 4;
( 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, A94, XBOOLE_1:1;
( 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:48, PRE_TOPC:29;
then A176:
F2 is
closed
by TSEP_1:8;
I[01] | SS is
SubSpace of
I[01] | S1
by A109, A136, A174, 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, A109, A136, A173, A175, A176, A134, A133, A120, TOPALG_3:20;
hence
Fn1 is
continuous
;
( 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, A135, A112, XBOOLE_1:28, ZFMISC_1:119;
hence
F | [:N1,S1:] = CircleMap * Fn1
by A161, A163, FUNCT_1:68, RELAT_1:46;
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:90
.=
[:( the carrier of Y /\ N1),({0} /\ the carrier of I[01]):]
by A8, ZFMISC_1:123
.=
[: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 A140, A141, FUNCT_1:9;
verum end;
end;
A177:
S2[
0 ]
by FINSEQ_3:26;
for
i being
Element of
NAT holds
S2[
i]
from NAT_1:sch 1(A177, 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 A178:
S = [.0,(TT . (len TT)).]
and A179:
y in N2
and A180:
N2 c= N
and A181:
Fn1 is
continuous
and A182:
F | [:N2,S:] = CircleMap * Fn1
and A183:
Fn1 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
by A17;
reconsider z =
Fn1 . x as
Point of
R^1 by TOPMETR:24;
A184:
I[01] | S = I[01]
by A12, A178, Lm6, BORSUK_1:83, TSEP_1:3;
then reconsider Fn1 =
Fn1 as
Function of
[:(Y | N2),I[01]:],
R^1 ;
take
z
;
S1[x,z]
take
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
( 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
;
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
;
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
;
( 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, A178, A179, A181, A182, A183, A184, BORSUK_1:83;
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;
( 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 A185:
H is
continuous
and A186:
F | [:N2, the carrier of I[01]:] = CircleMap * H
and A187:
H | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
;
Fn1 = H
defpred S3[
Element of
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:] ) );
A188:
dom Fn1 = the
carrier of
[:(Y | N2),I[01]:]
by FUNCT_2:def 1;
A189:
( 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 5, PRE_TOPC:29;
A190:
dom H = the
carrier of
[:(Y | N2),I[01]:]
by FUNCT_2:def 1;
A191:
for
i being
Element of
NAT st
S3[
i] holds
S3[
i + 1]
proof
let i be
Element of
NAT ;
( S3[i] implies S3[i + 1] )
assume that A192:
S3[
i]
and A193:
i + 1
in dom TT
;
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 A193, TOPREALA:23;
suppose A194:
i = 0
;
ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )set Z =
[.0,(TT . (i + 1)).];
A195:
[.0,(TT . (i + 1)).] = {0}
by A11, A194, XXREAL_1:17;
reconsider Z =
[.0,(TT . (i + 1)).] as non
empty Subset of
I[01] by A11, A194, Lm3, XXREAL_1:17;
A196:
[:N2,Z:] c= [:N2, the carrier of I[01]:]
by ZFMISC_1:118;
then A197:
dom (Fn1 | [:N2,Z:]) = [:N2,Z:]
by A189, A188, RELAT_1:91;
A198:
for
x being
set st
x in dom (Fn1 | [:N2,Z:]) holds
(Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
proof
let x be
set ;
( x in dom (Fn1 | [:N2,Z:]) implies (Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x )
A199:
[:N2,Z:] c= [: the carrier of Y,Z:]
by ZFMISC_1:118;
assume A200:
x in dom (Fn1 | [:N2,Z:])
;
(Fn1 | [:N2,Z:]) . x = (H | [:N2,Z:]) . x
hence (Fn1 | [:N2,Z:]) . x =
Fn1 . x
by A197, FUNCT_1:72
.=
(Fn1 | [: the carrier of Y,{0}:]) . x
by A195, A197, A200, A199, FUNCT_1:72
.=
H . x
by A183, A187, A195, A197, A200, A199, FUNCT_1:72
.=
(H | [:N2,Z:]) . x
by A197, A200, FUNCT_1:72
;
verum
end; take
Z
;
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )thus
Z = [.0,(TT . (i + 1)).]
;
Fn1 | [:N2,Z:] = H | [:N2,Z:]
dom (H | [:N2,Z:]) = [:N2,Z:]
by A190, A189, A196, RELAT_1:91;
hence
Fn1 | [:N2,Z:] = H | [:N2,Z:]
by A188, A198, FUNCT_1:9, RELAT_1:91;
verum end; suppose A201:
i in dom TT
;
ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z:] = H | [:N2,Z:] )set ZZ =
[.(TT . i),(TT . (i + 1)).];
A202:
0 <= TT . i
by A19, A201;
A203:
TT . (i + 1) <= 1
by A19, A193, A201;
then reconsider ZZ =
[.(TT . i),(TT . (i + 1)).] as
Subset of
I[01] by A25, A202;
consider Z being non
empty Subset of
I[01] such that A204:
Z = [.0,(TT . i).]
and A205:
Fn1 | [:N2,Z:] = H | [:N2,Z:]
by A192, A201;
take Z1 =
Z \/ ZZ;
( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:N2,Z1:] = H | [:N2,Z1:] )A206:
TT . i < TT . (i + 1)
by A19, A193, A201;
hence
Z1 = [.0,(TT . (i + 1)).]
by A204, A202, XXREAL_1:165;
Fn1 | [:N2,Z1:] = H | [:N2,Z1:]A207:
[:N2,Z1:] c= [:N2, the carrier of I[01]:]
by ZFMISC_1:118;
then A208:
dom (Fn1 | [:N2,Z1:]) = [:N2,Z1:]
by A189, A188, RELAT_1:91;
A209:
for
x being
set st
x in dom (Fn1 | [:N2,Z1:]) holds
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
proof
0 <= TT . (i + 1)
by A19, A193;
then A210:
TT . (i + 1) is
Point of
I[01]
by A203, BORSUK_1:86;
(
0 <= TT . i &
TT . i <= 1 )
by A19, A193, A201;
then
TT . i is
Point of
I[01]
by BORSUK_1:86;
then A211:
ZZ is
connected
by A206, A210, BORSUK_4:49;
consider Ui being non
empty Subset of
(Tunit_circle 2) such that A212:
Ui in UL
and A213:
F .: [:N,ZZ:] c= Ui
by A16, A193, A201;
consider D being
mutually-disjoint open Subset-Family of
R^1 such that A214:
union D = CircleMap " Ui
and A215:
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, A212;
let x be
set ;
( x in dom (Fn1 | [:N2,Z1:]) implies (Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x )
assume A216:
x in dom (Fn1 | [:N2,Z1:])
;
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . x
consider x1,
x2 being
set such that A217:
x1 in N2
and A218:
x2 in Z1
and A219:
x = [x1,x2]
by A208, A216, ZFMISC_1:def 2;
A220:
TT . i in ZZ
by A206, XXREAL_1:1;
then
[x1,(TT . i)] in [:N,ZZ:]
by A180, A217, ZFMISC_1:106;
then A221:
F . [x1,(TT . i)] in F .: [:N,ZZ:]
by FUNCT_2:43;
reconsider xy =
{x1} as non
empty Subset of
Y by A217, ZFMISC_1:37;
A222:
xy c= N2
by A217, ZFMISC_1:37;
then reconsider xZZ =
[:xy,ZZ:] as
Subset of
[:(Y | N2),I[01]:] by A189, ZFMISC_1:119;
A223:
dom (H | [:xy,ZZ:]) = [:xy,ZZ:]
by A190, A189, A222, RELAT_1:91, ZFMISC_1:119;
A224:
D is
Cover of
Fn1 .: xZZ
proof
let b be
set ;
TARSKI:def 3,
SETFAM_1:def 12 ( not b in Fn1 .: xZZ or b in union D )
A225:
[:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:]
by ZFMISC_1:119;
assume
b in Fn1 .: xZZ
;
b in union D
then consider a being
Point of
[:(Y | N2),I[01]:] such that A226:
a in xZZ
and A227:
Fn1 . a = b
by FUNCT_2:116;
xy c= N
by A180, A217, ZFMISC_1:37;
then
[:xy,ZZ:] c= [:N,ZZ:]
by ZFMISC_1:118;
then
a in [:N,ZZ:]
by A226;
then A228:
F . a in F .: [:N,ZZ:]
by A6, A225, FUNCT_1:def 12;
CircleMap . (Fn1 . a) =
(CircleMap * Fn1) . a
by FUNCT_2:21
.=
F . a
by A12, A178, A182, A189, BORSUK_1:83, FUNCT_1:72
;
hence
b in union D
by A213, A214, A227, A228, Lm12, FUNCT_1:def 13, TOPMETR:24;
verum
end;
A229:
D is
Cover of
H .: xZZ
proof
let b be
set ;
TARSKI:def 3,
SETFAM_1:def 12 ( not b in H .: xZZ or b in union D )
A230:
[:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:]
by ZFMISC_1:119;
assume
b in H .: xZZ
;
b in union D
then consider a being
Point of
[:(Y | N2),I[01]:] such that A231:
a in xZZ
and A232:
H . a = b
by FUNCT_2:116;
A233:
CircleMap . (H . a) =
(CircleMap * H) . a
by FUNCT_2:21
.=
F . a
by A186, A189, FUNCT_1:72
;
xy c= N
by A180, A217, ZFMISC_1:37;
then
[:xy,ZZ:] c= [:N,ZZ:]
by ZFMISC_1:118;
then
a in [:N,ZZ:]
by A231;
then
F . a in F .: [:N,ZZ:]
by A6, A230, FUNCT_1:def 12;
hence
b in union D
by A213, A214, A232, A233, Lm12, FUNCT_1:def 13, TOPMETR:24;
verum
end;
TT . i in Z
by A204, A202, XXREAL_1:1;
then A234:
[x1,(TT . i)] in [:N2,Z:]
by A217, ZFMISC_1:106;
then A235:
Fn1 . [x1,(TT . i)] =
(Fn1 | [:N2,Z:]) . [x1,(TT . i)]
by FUNCT_1:72
.=
H . [x1,(TT . i)]
by A205, A234, FUNCT_1:72
;
A236:
[:N2,Z:] c= [:N2, the carrier of I[01]:]
by ZFMISC_1:118;
then F . [x1,(TT . i)] =
(CircleMap * H) . [x1,(TT . i)]
by A186, A234, FUNCT_1:72
.=
CircleMap . (H . [x1,(TT . i)])
by A190, A189, A234, A236, FUNCT_1:23
;
then
H . [x1,(TT . i)] in CircleMap " Ui
by A213, A221, FUNCT_2:46, TOPMETR:24;
then consider Uith being
set such that A237:
H . [x1,(TT . i)] in Uith
and A238:
Uith in D
by A214, TARSKI:def 4;
F . [x1,(TT . i)] =
(CircleMap * Fn1) . [x1,(TT . i)]
by A12, A178, A182, A234, A236, BORSUK_1:83, FUNCT_1:72
.=
CircleMap . (Fn1 . [x1,(TT . i)])
by A189, A188, A234, A236, FUNCT_1:23
;
then
Fn1 . [x1,(TT . i)] in CircleMap " Ui
by A213, A221, FUNCT_2:46, TOPMETR:24;
then consider Uit being
set such that A239:
Fn1 . [x1,(TT . i)] in Uit
and A240:
Uit in D
by A214, TARSKI:def 4;
I[01] is
SubSpace of
I[01]
by TSEP_1:2;
then A241:
[:(Y | N2),I[01]:] is
SubSpace of
[:Y,I[01]:]
by BORSUK_3:25;
xy is
connected
by A217;
then
[:xy,ZZ:] is
connected
by A211, TOPALG_3:17;
then A242:
xZZ is
connected
by A241, CONNSP_1:24;
reconsider Uith =
Uith as non
empty Subset of
R^1 by A237, A238;
A243:
x1 in xy
by TARSKI:def 1;
then A244:
[x1,(TT . i)] in xZZ
by A220, ZFMISC_1:106;
then
H . [x1,(TT . i)] in H .: xZZ
by FUNCT_2:43;
then
Uith meets H .: xZZ
by A237, XBOOLE_0:3;
then A245:
H .: xZZ c= Uith
by A185, A242, A238, A229, TOPALG_3:13, TOPS_2:75;
reconsider Uit =
Uit as non
empty Subset of
R^1 by A239, A240;
set f =
CircleMap | Uit;
A246:
dom (CircleMap | Uit) = Uit
by Lm12, RELAT_1:91, TOPMETR:24;
A247:
rng (CircleMap | Uit) c= Ui
( the
carrier of
((Tunit_circle 2) | Ui) = Ui & the
carrier of
(R^1 | Uit) = Uit )
by PRE_TOPC:29;
then reconsider f =
CircleMap | Uit as
Function of
(R^1 | Uit),
((Tunit_circle 2) | Ui) by A246, A247, FUNCT_2:4;
A250:
dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:]
by A189, A188, A222, RELAT_1:91, ZFMISC_1:119;
H . [x1,(TT . i)] in H .: xZZ
by A190, A244, FUNCT_1:def 12;
then
Uit meets Uith
by A239, A245, A235, XBOOLE_0:3;
then A251:
Uit = Uith
by A240, A238, TAXONOM2:def 5;
A252:
rng (H | [:xy,ZZ:]) c= dom f
proof
let b be
set ;
TARSKI:def 3 ( not b in rng (H | [:xy,ZZ:]) or b in dom f )
assume
b in rng (H | [:xy,ZZ:])
;
b in dom f
then consider a being
set such that A253:
a in dom (H | [:xy,ZZ:])
and A254:
(H | [:xy,ZZ:]) . a = b
by FUNCT_1:def 5;
H . a = b
by A223, A253, A254, FUNCT_1:72;
then
b in H .: xZZ
by A190, A223, A253, FUNCT_1:def 12;
hence
b in dom f
by A245, A251, A246;
verum
end;
Fn1 . [x1,(TT . i)] in Fn1 .: xZZ
by A244, FUNCT_2:43;
then
Uit meets Fn1 .: xZZ
by A239, XBOOLE_0:3;
then A255:
Fn1 .: xZZ c= Uit
by A181, A184, A240, A242, A224, TOPALG_3:13, TOPS_2:75;
A256:
rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be
set ;
TARSKI:def 3 ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume
b in rng (Fn1 | [:xy,ZZ:])
;
b in dom f
then consider a being
set such that A257:
a in dom (Fn1 | [:xy,ZZ:])
and A258:
(Fn1 | [:xy,ZZ:]) . a = b
by FUNCT_1:def 5;
Fn1 . a = b
by A250, A257, A258, FUNCT_1:72;
then
b in Fn1 .: xZZ
by A188, A250, A257, FUNCT_1:def 12;
hence
b in dom f
by A255, A246;
verum
end;
then A259:
dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:])
by RELAT_1:46;
A260:
for
x being
set st
x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
proof
let x be
set ;
( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x )
assume A261:
x in dom (f * (Fn1 | [:xy,ZZ:]))
;
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (H | [:xy,ZZ:])) . x
A262:
Fn1 . x in Fn1 .: [:xy,ZZ:]
by A188, A250, A259, A261, FUNCT_1:def 12;
A263:
H . x in H .: [:xy,ZZ:]
by A190, A250, A259, A261, FUNCT_1:def 12;
thus (f * (Fn1 | [:xy,ZZ:])) . x =
((f * Fn1) | [:xy,ZZ:]) . x
by RELAT_1:112
.=
(f * Fn1) . x
by A250, A259, A261, FUNCT_1:72
.=
f . (Fn1 . x)
by A188, A261, FUNCT_1:23
.=
CircleMap . (Fn1 . x)
by A255, A262, FUNCT_1:72
.=
(CircleMap * Fn1) . x
by A188, A261, FUNCT_1:23
.=
CircleMap . (H . x)
by A12, A178, A182, A186, A190, A261, BORSUK_1:83, FUNCT_1:23
.=
f . (H . x)
by A245, A251, A263, FUNCT_1:72
.=
(f * H) . x
by A190, A261, FUNCT_1:23
.=
((f * H) | [:xy,ZZ:]) . x
by A250, A259, A261, FUNCT_1:72
.=
(f * (H | [:xy,ZZ:])) . x
by RELAT_1:112
;
verum
end;
f is
being_homeomorphism
by A215, A240;
then A264:
f is
one-to-one
by TOPS_2:def 5;
dom (f * (H | [:xy,ZZ:])) = dom (H | [:xy,ZZ:])
by A252, RELAT_1:46;
then A265:
f * (Fn1 | [:xy,ZZ:]) = f * (H | [:xy,ZZ:])
by A250, A223, A256, A260, FUNCT_1:9, RELAT_1:46;
per cases
( x2 in ZZ or not x2 in ZZ )
;
suppose
x2 in ZZ
;
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . xthen A266:
x in [:xy,ZZ:]
by A219, A243, ZFMISC_1:106;
thus (Fn1 | [:N2,Z1:]) . x =
Fn1 . x
by A208, A216, FUNCT_1:72
.=
(Fn1 | [:xy,ZZ:]) . x
by A266, FUNCT_1:72
.=
(H | [:xy,ZZ:]) . x
by A264, A250, A223, A256, A252, A265, FUNCT_1:49
.=
H . x
by A266, FUNCT_1:72
.=
(H | [:N2,Z1:]) . x
by A208, A216, FUNCT_1:72
;
verum end; suppose
not
x2 in ZZ
;
(Fn1 | [:N2,Z1:]) . x = (H | [:N2,Z1:]) . xthen
x2 in Z
by A218, XBOOLE_0:def 3;
then A267:
x in [:N2,Z:]
by A217, A219, ZFMISC_1:106;
thus (Fn1 | [:N2,Z1:]) . x =
Fn1 . x
by A208, A216, FUNCT_1:72
.=
(Fn1 | [:N2,Z:]) . x
by A267, FUNCT_1:72
.=
H . x
by A205, A267, FUNCT_1:72
.=
(H | [:N2,Z1:]) . x
by A208, A216, FUNCT_1:72
;
verum end;
end;
dom (H | [:N2,Z1:]) = [:N2,Z1:]
by A190, A189, A207, RELAT_1:91;
hence
Fn1 | [:N2,Z1:] = H | [:N2,Z1:]
by A188, A209, FUNCT_1:9, RELAT_1:91;
verum end;
end;
A268:
S3[
0 ]
by FINSEQ_3:26;
for
i being
Element of
NAT holds
S3[
i]
from NAT_1:sch 1(A268, A191);
then consider Z being non
empty Subset of
I[01] such that A269:
Z = [.0,(TT . (len TT)).]
and A270:
Fn1 | [:N2,Z:] = H | [:N2,Z:]
by A17;
thus Fn1 =
Fn1 | [:N2,Z:]
by A12, A189, A188, A269, BORSUK_1:83, RELAT_1:98
.=
H
by A12, A190, A189, A269, A270, BORSUK_1:83, RELAT_1:98
;
verum
end;
consider G being Function of [:Y,I[01]:],R^1 such that
A271:
for x being Point of [:Y,I[01]:] holds S1[x,G . x]
from FUNCT_2:sch 3(A9);
take
G
; ( 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 ) )
A273:
for p being Point of [:Y,I[01]:]
for y being Point of Y
for t being Point of I[01]
for N1, N2 being non empty open Subset of Y
for Fn1 being Function of [:(Y | N1),I[01]:],R^1
for Fn2 being Function of [:(Y | N2),I[01]:],R^1 st p = [y,t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & F | [:N2, the carrier of I[01]:] = CircleMap * Fn2 & Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:] & F | [:N1, the carrier of I[01]:] = CircleMap * Fn1 & Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:] holds
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
proof
let p be
Point of
[:Y,I[01]:];
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;
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];
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;
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;
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;
( 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 A274:
y in N1
and A275:
y in N2
and A276:
Fn2 is
continuous
and A277:
Fn1 is
continuous
and A278:
F | [:N2, the carrier of I[01]:] = CircleMap * Fn2
and A279:
Fn2 | [: the carrier of Y,{0}:] = Ft | [:N2, the carrier of I[01]:]
and A280:
F | [:N1, the carrier of I[01]:] = CircleMap * Fn1
and A281:
Fn1 | [: the carrier of Y,{0}:] = Ft | [:N1, the carrier of I[01]:]
;
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
A282:
{y} c= N1
by A274, ZFMISC_1:37;
consider TT being non
empty FinSequence of
REAL such that A283:
TT . 1
= 0
and A284:
TT . (len TT) = 1
and A285:
TT is
increasing
and A286:
ex
N being
open Subset of
Y st
(
y in N & ( for
i being
natural number 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 A287:
y in N
and A288:
for
i being
natural number 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 A286;
reconsider N =
N as non
empty open Subset of
Y by A287;
defpred S2[
Element of
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:] ) );
A289:
len TT in dom TT
by FINSEQ_5:6;
A290:
dom Fn2 = the
carrier of
[:(Y | N2),I[01]:]
by FUNCT_2:def 1;
A291:
dom Fn2 = [:N2, the carrier of I[01]:]
by A272;
A292:
{y} c= N2
by A275, ZFMISC_1:37;
A293:
( 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 5, PRE_TOPC:29;
A294:
( 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 5, PRE_TOPC:29;
A295:
dom Fn1 = [:N1, the carrier of I[01]:]
by A272;
A296:
dom Fn1 = the
carrier of
[:(Y | N1),I[01]:]
by FUNCT_2:def 1;
A297:
1
in dom TT
by FINSEQ_5:6;
A298:
for
i being
Element of
NAT st
S2[
i] holds
S2[
i + 1]
proof
let i be
Element of
NAT ;
( S2[i] implies S2[i + 1] )
assume that A299:
S2[
i]
and A300:
i + 1
in dom TT
;
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 A300, TOPREALA:23;
suppose A301:
i = 0
;
ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )set Z =
[.0,(TT . (i + 1)).];
A302:
[.0,(TT . (i + 1)).] = {0}
by A283, A301, XXREAL_1:17;
reconsider Z =
[.0,(TT . (i + 1)).] as non
empty Subset of
I[01] by A283, A301, Lm3, XXREAL_1:17;
A303:
[:{y},Z:] c= [:N2, the carrier of I[01]:]
by A292, ZFMISC_1:119;
A304:
dom (Fn1 | [:{y},Z:]) = [:{y},Z:]
by A282, A295, RELAT_1:91, ZFMISC_1:119;
A305:
[:{y},Z:] c= [:N1, the carrier of I[01]:]
by A282, ZFMISC_1:119;
A306:
for
x being
set st
x in dom (Fn1 | [:{y},Z:]) holds
(Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
proof
let x be
set ;
( x in dom (Fn1 | [:{y},Z:]) implies (Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x )
A307:
[:{y},Z:] c= [: the carrier of Y,Z:]
by ZFMISC_1:118;
assume A308:
x in dom (Fn1 | [:{y},Z:])
;
(Fn1 | [:{y},Z:]) . x = (Fn2 | [:{y},Z:]) . x
hence (Fn1 | [:{y},Z:]) . x =
Fn1 . x
by A304, FUNCT_1:72
.=
(Fn1 | [: the carrier of Y,{0}:]) . x
by A302, A304, A308, A307, FUNCT_1:72
.=
Ft . x
by A281, A305, A304, A308, FUNCT_1:72
.=
(Ft | [:N2, the carrier of I[01]:]) . x
by A304, A303, A308, FUNCT_1:72
.=
Fn2 . x
by A279, A302, A304, A308, A307, FUNCT_1:72
.=
(Fn2 | [:{y},Z:]) . x
by A304, A308, FUNCT_1:72
;
verum
end; take
Z
;
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )thus
Z = [.0,(TT . (i + 1)).]
;
Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]
dom (Fn2 | [:{y},Z:]) = [:{y},Z:]
by A292, A291, RELAT_1:91, ZFMISC_1:119;
hence
Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]
by A304, A306, FUNCT_1:9;
verum end; suppose A309:
i in dom TT
;
ex Z being non empty Subset of I[01] st
( Z = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )A310:
now let i be
Element of
NAT ;
( 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 A311:
i in dom TT
;
( 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 A311, FINSEQ_3:27;
then
( 1
= i or 1
< i )
by XXREAL_0:1;
hence A312:
0 <= TT . i
by A283, A285, A297, A311, SEQM_3:def 1;
( i + 1 in dom TT implies ( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) ) )assume A313:
i + 1
in dom TT
;
( TT . i < TT . (i + 1) & TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )A314:
i + 0 < i + 1
by XREAL_1:10;
hence A315:
TT . i < TT . (i + 1)
by A285, A311, A313, SEQM_3:def 1;
( TT . (i + 1) <= 1 & TT . i < 1 & 0 < TT . (i + 1) )
i + 1
<= len TT
by A313, FINSEQ_3:27;
then
(
i + 1
= len TT or
i + 1
< len TT )
by XXREAL_0:1;
hence
TT . (i + 1) <= 1
by A284, A285, A289, A313, SEQM_3:def 1;
( TT . i < 1 & 0 < TT . (i + 1) )hence
TT . i < 1
by A315, XXREAL_0:2;
0 < TT . (i + 1)thus
0 < TT . (i + 1)
by A285, A311, A312, A313, A314, SEQM_3:def 1;
verum end; then A316:
0 <= TT . i
by A309;
A317:
TT . (i + 1) <= 1
by A300, A309, A310;
set ZZ =
[.(TT . i),(TT . (i + 1)).];
consider Z being non
empty Subset of
I[01] such that A318:
Z = [.0,(TT . i).]
and A319:
Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:]
by A299, A309;
then reconsider ZZ =
[.(TT . i),(TT . (i + 1)).] as
Subset of
I[01] by A316, A317;
take Z1 =
Z \/ ZZ;
( Z1 = [.0,(TT . (i + 1)).] & Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:] )A324:
TT . i < TT . (i + 1)
by A300, A309, A310;
hence
Z1 = [.0,(TT . (i + 1)).]
by A318, A316, XXREAL_1:165;
Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]A325:
dom (Fn1 | [:{y},Z1:]) = [:{y},Z1:]
by A282, A295, RELAT_1:91, ZFMISC_1:119;
A326:
for
x being
set st
x in dom (Fn1 | [:{y},Z1:]) holds
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
proof
0 <= TT . (i + 1)
by A300, A310;
then A327:
TT . (i + 1) is
Point of
I[01]
by A317, BORSUK_1:86;
(
0 <= TT . i &
TT . i <= 1 )
by A300, A309, A310;
then
TT . i is
Point of
I[01]
by BORSUK_1:86;
then A328:
ZZ is
connected
by A324, A327, BORSUK_4:49;
A329:
TT . i in ZZ
by A324, XXREAL_1:1;
consider Ui being non
empty Subset of
(Tunit_circle 2) such that A330:
Ui in UL
and A331:
F .: [:N,ZZ:] c= Ui
by A288, A300, A309;
consider D being
mutually-disjoint open Subset-Family of
R^1 such that A332:
union D = CircleMap " Ui
and A333:
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, A330;
let x be
set ;
( x in dom (Fn1 | [:{y},Z1:]) implies (Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x )
assume A334:
x in dom (Fn1 | [:{y},Z1:])
;
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . x
consider x1,
x2 being
set such that A335:
x1 in {y}
and A336:
x2 in Z1
and A337:
x = [x1,x2]
by A325, A334, ZFMISC_1:def 2;
reconsider xy =
{x1} as non
empty Subset of
Y by A335, ZFMISC_1:37;
A338:
xy c= N2
by A292, A335, ZFMISC_1:37;
then A339:
[:xy,ZZ:] c= [:N2, the carrier of I[01]:]
by ZFMISC_1:119;
A340:
x1 = y
by A335, TARSKI:def 1;
then
[x1,(TT . i)] in [:N,ZZ:]
by A287, A329, ZFMISC_1:106;
then A341:
F . [x1,(TT . i)] in F .: [:N,ZZ:]
by FUNCT_2:43;
A342:
xy c= N1
by A282, A335, ZFMISC_1:37;
then reconsider xZZ =
[:xy,ZZ:] as
Subset of
[:(Y | N1),I[01]:] by A293, ZFMISC_1:119;
xy is
connected
by A335;
then A343:
[:xy,ZZ:] is
connected
by A328, TOPALG_3:17;
A344:
xy c= N
by A287, A340, ZFMISC_1:37;
A345:
D is
Cover of
Fn1 .: xZZ
proof
let b be
set ;
TARSKI:def 3,
SETFAM_1:def 12 ( not b in Fn1 .: xZZ or b in union D )
A346:
[:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:]
by ZFMISC_1:119;
assume
b in Fn1 .: xZZ
;
b in union D
then consider a being
Point of
[:(Y | N1),I[01]:] such that A347:
a in xZZ
and A348:
Fn1 . a = b
by FUNCT_2:116;
A349:
CircleMap . (Fn1 . a) =
(CircleMap * Fn1) . a
by FUNCT_2:21
.=
F . a
by A280, A293, FUNCT_1:72
;
[:xy,ZZ:] c= [:N,ZZ:]
by A344, ZFMISC_1:118;
then
a in [:N,ZZ:]
by A347;
then
F . a in F .: [:N,ZZ:]
by A6, A346, FUNCT_1:def 12;
hence
b in union D
by A331, A332, A348, A349, Lm12, FUNCT_1:def 13, TOPMETR:24;
verum
end;
A350:
I[01] is
SubSpace of
I[01]
by TSEP_1:2;
then
[:(Y | N1),I[01]:] is
SubSpace of
[:Y,I[01]:]
by BORSUK_3:25;
then A351:
xZZ is
connected
by A343, CONNSP_1:24;
reconsider XZZ =
[:xy,ZZ:] as
Subset of
[:(Y | N2),I[01]:] by A294, A338, ZFMISC_1:119;
[:(Y | N2),I[01]:] is
SubSpace of
[:Y,I[01]:]
by A350, BORSUK_3:25;
then A352:
XZZ is
connected
by A343, CONNSP_1:24;
A353:
D is
Cover of
Fn2 .: xZZ
proof
let b be
set ;
TARSKI:def 3,
SETFAM_1:def 12 ( not b in Fn2 .: xZZ or b in union D )
A354:
[:N,ZZ:] c= [: the carrier of Y, the carrier of I[01]:]
by ZFMISC_1:119;
assume
b in Fn2 .: xZZ
;
b in union D
then consider a being
Point of
[:(Y | N2),I[01]:] such that A355:
a in xZZ
and A356:
Fn2 . a = b
by FUNCT_2:116;
A357:
CircleMap . (Fn2 . a) =
(CircleMap * Fn2) . a
by FUNCT_2:21
.=
F . a
by A278, A294, FUNCT_1:72
;
[:xy,ZZ:] c= [:N,ZZ:]
by A344, ZFMISC_1:118;
then
a in [:N,ZZ:]
by A355;
then
F . a in F .: [:N,ZZ:]
by A6, A354, FUNCT_1:def 12;
hence
b in union D
by A331, A332, A356, A357, Lm12, FUNCT_1:def 13, TOPMETR:24;
verum
end;
A358:
TT . i in Z
by A318, A316, XXREAL_1:1;
then A359:
[x1,(TT . i)] in [:{y},Z:]
by A335, ZFMISC_1:106;
A360:
[:{y},Z:] c= [:N1, the carrier of I[01]:]
by A282, ZFMISC_1:119;
then F . [x1,(TT . i)] =
(CircleMap * Fn1) . [x1,(TT . i)]
by A280, A359, FUNCT_1:72
.=
CircleMap . (Fn1 . [x1,(TT . i)])
by A295, A359, A360, FUNCT_1:23
;
then
Fn1 . [x1,(TT . i)] in CircleMap " Ui
by A331, A341, FUNCT_2:46, TOPMETR:24;
then consider Uit being
set such that A361:
Fn1 . [x1,(TT . i)] in Uit
and A362:
Uit in D
by A332, TARSKI:def 4;
reconsider Uit =
Uit as non
empty Subset of
R^1 by A361, A362;
set f =
CircleMap | Uit;
A363:
dom (CircleMap | Uit) = Uit
by Lm12, RELAT_1:91, TOPMETR:24;
A364:
rng (CircleMap | Uit) c= Ui
( the
carrier of
((Tunit_circle 2) | Ui) = Ui & the
carrier of
(R^1 | Uit) = Uit )
by PRE_TOPC:29;
then reconsider f =
CircleMap | Uit as
Function of
(R^1 | Uit),
((Tunit_circle 2) | Ui) by A363, A364, FUNCT_2:4;
A367:
[:N2,Z:] c= [:N2, the carrier of I[01]:]
by ZFMISC_1:118;
A368:
[x1,(TT . i)] in [:N2,Z:]
by A292, A335, A358, ZFMISC_1:106;
then F . [x1,(TT . i)] =
(CircleMap * Fn2) . [x1,(TT . i)]
by A278, A367, FUNCT_1:72
.=
CircleMap . (Fn2 . [x1,(TT . i)])
by A290, A294, A368, A367, FUNCT_1:23
;
then
Fn2 . [x1,(TT . i)] in CircleMap " Ui
by A331, A341, FUNCT_2:46, TOPMETR:24;
then consider Uith being
set such that A369:
Fn2 . [x1,(TT . i)] in Uith
and A370:
Uith in D
by A332, TARSKI:def 4;
reconsider Uith =
Uith as non
empty Subset of
R^1 by A369, A370;
A371:
dom (Fn1 | [:xy,ZZ:]) = [:xy,ZZ:]
by A293, A296, A342, RELAT_1:91, ZFMISC_1:119;
A372:
x1 in xy
by TARSKI:def 1;
then A373:
[x1,(TT . i)] in xZZ
by A329, ZFMISC_1:106;
then
Fn1 . [x1,(TT . i)] in Fn1 .: xZZ
by FUNCT_2:43;
then
Uit meets Fn1 .: xZZ
by A361, XBOOLE_0:3;
then A374:
Fn1 .: xZZ c= Uit
by A277, A362, A351, A345, TOPALG_3:13, TOPS_2:75;
A375:
rng (Fn1 | [:xy,ZZ:]) c= dom f
proof
let b be
set ;
TARSKI:def 3 ( not b in rng (Fn1 | [:xy,ZZ:]) or b in dom f )
assume
b in rng (Fn1 | [:xy,ZZ:])
;
b in dom f
then consider a being
set such that A376:
a in dom (Fn1 | [:xy,ZZ:])
and A377:
(Fn1 | [:xy,ZZ:]) . a = b
by FUNCT_1:def 5;
Fn1 . a = b
by A371, A376, A377, FUNCT_1:72;
then
b in Fn1 .: xZZ
by A296, A371, A376, FUNCT_1:def 12;
hence
b in dom f
by A374, A363;
verum
end;
then A378:
dom (f * (Fn1 | [:xy,ZZ:])) = dom (Fn1 | [:xy,ZZ:])
by RELAT_1:46;
[x1,(TT . i)] in [:xy,ZZ:]
by A335, A340, A329, ZFMISC_1:106;
then
[x1,(TT . i)] in dom Fn2
by A291, A339;
then A379:
Fn2 . [x1,(TT . i)] in Fn2 .: xZZ
by A373, FUNCT_2:43;
then
Uith meets Fn2 .: xZZ
by A369, XBOOLE_0:3;
then A380:
Fn2 .: xZZ c= Uith
by A276, A370, A352, A353, TOPALG_3:13, TOPS_2:75;
Fn1 . [x1,(TT . i)] =
(Fn1 | [:{y},Z:]) . [x1,(TT . i)]
by A359, FUNCT_1:72
.=
Fn2 . [x1,(TT . i)]
by A319, A359, FUNCT_1:72
;
then
Uit meets Uith
by A361, A379, A380, XBOOLE_0:3;
then A381:
Uit = Uith
by A362, A370, TAXONOM2:def 5;
A382:
for
x being
set st
x in dom (f * (Fn1 | [:xy,ZZ:])) holds
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
proof
A383:
dom (Fn1 | [:xy,ZZ:]) c= dom Fn1
by RELAT_1:89;
let x be
set ;
( x in dom (f * (Fn1 | [:xy,ZZ:])) implies (f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x )
assume A384:
x in dom (f * (Fn1 | [:xy,ZZ:]))
;
(f * (Fn1 | [:xy,ZZ:])) . x = (f * (Fn2 | [:xy,ZZ:])) . x
A385:
Fn1 . x in Fn1 .: [:xy,ZZ:]
by A296, A371, A378, A384, FUNCT_1:def 12;
A386:
Fn2 . x in Fn2 .: [:xy,ZZ:]
by A291, A339, A371, A378, A384, FUNCT_1:def 12;
dom (Fn1 | [:xy,ZZ:]) = (dom Fn1) /\ [:xy,ZZ:]
by RELAT_1:90;
then A387:
x in [:xy,ZZ:]
by A378, A384, XBOOLE_0:def 4;
thus (f * (Fn1 | [:xy,ZZ:])) . x =
((f * Fn1) | [:xy,ZZ:]) . x
by RELAT_1:112
.=
(f * Fn1) . x
by A371, A378, A384, FUNCT_1:72
.=
f . (Fn1 . x)
by A296, A384, FUNCT_1:23
.=
CircleMap . (Fn1 . x)
by A374, A385, FUNCT_1:72
.=
(CircleMap * Fn1) . x
by A296, A384, FUNCT_1:23
.=
F . x
by A280, A295, A378, A384, A383, FUNCT_1:72
.=
(CircleMap * Fn2) . x
by A278, A339, A387, FUNCT_1:72
.=
CircleMap . (Fn2 . x)
by A291, A339, A387, FUNCT_1:23
.=
f . (Fn2 . x)
by A380, A381, A386, FUNCT_1:72
.=
(f * Fn2) . x
by A291, A339, A387, FUNCT_1:23
.=
((f * Fn2) | [:xy,ZZ:]) . x
by A371, A378, A384, FUNCT_1:72
.=
(f * (Fn2 | [:xy,ZZ:])) . x
by RELAT_1:112
;
verum
end;
A388:
dom (Fn2 | [:xy,ZZ:]) = [:xy,ZZ:]
by A290, A294, A338, RELAT_1:91, ZFMISC_1:119;
A389:
rng (Fn2 | [:xy,ZZ:]) c= dom f
proof
let b be
set ;
TARSKI:def 3 ( not b in rng (Fn2 | [:xy,ZZ:]) or b in dom f )
assume
b in rng (Fn2 | [:xy,ZZ:])
;
b in dom f
then consider a being
set such that A390:
a in dom (Fn2 | [:xy,ZZ:])
and A391:
(Fn2 | [:xy,ZZ:]) . a = b
by FUNCT_1:def 5;
Fn2 . a = b
by A388, A390, A391, FUNCT_1:72;
then
b in Fn2 .: xZZ
by A290, A388, A390, FUNCT_1:def 12;
hence
b in dom f
by A380, A381, A363;
verum
end;
then
dom (f * (Fn2 | [:xy,ZZ:])) = dom (Fn2 | [:xy,ZZ:])
by RELAT_1:46;
then A392:
f * (Fn1 | [:xy,ZZ:]) = f * (Fn2 | [:xy,ZZ:])
by A371, A388, A375, A382, FUNCT_1:9, RELAT_1:46;
f is
being_homeomorphism
by A333, A362;
then A393:
f is
one-to-one
by TOPS_2:def 5;
per cases
( x2 in ZZ or not x2 in ZZ )
;
suppose
x2 in ZZ
;
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . xthen A394:
x in [:xy,ZZ:]
by A337, A372, ZFMISC_1:106;
thus (Fn1 | [:{y},Z1:]) . x =
Fn1 . x
by A325, A334, FUNCT_1:72
.=
(Fn1 | [:xy,ZZ:]) . x
by A394, FUNCT_1:72
.=
(Fn2 | [:xy,ZZ:]) . x
by A393, A371, A388, A375, A389, A392, FUNCT_1:49
.=
Fn2 . x
by A394, FUNCT_1:72
.=
(Fn2 | [:{y},Z1:]) . x
by A325, A334, FUNCT_1:72
;
verum end; suppose
not
x2 in ZZ
;
(Fn1 | [:{y},Z1:]) . x = (Fn2 | [:{y},Z1:]) . xthen
x2 in Z
by A336, XBOOLE_0:def 3;
then A395:
x in [:{y},Z:]
by A335, A337, ZFMISC_1:106;
thus (Fn1 | [:{y},Z1:]) . x =
Fn1 . x
by A325, A334, FUNCT_1:72
.=
(Fn1 | [:{y},Z:]) . x
by A395, FUNCT_1:72
.=
Fn2 . x
by A319, A395, FUNCT_1:72
.=
(Fn2 | [:{y},Z1:]) . x
by A325, A334, FUNCT_1:72
;
verum end;
end;
dom (Fn2 | [:{y},Z1:]) = [:{y},Z1:]
by A292, A290, A294, RELAT_1:91, ZFMISC_1:119;
hence
Fn1 | [:{y},Z1:] = Fn2 | [:{y},Z1:]
by A325, A326, FUNCT_1:9;
verum
end;
A396:
S2[
0 ]
by FINSEQ_3:26;
for
i being
Element of
NAT holds
S2[
i]
from NAT_1:sch 1(A396, A298);
then
ex
Z being non
empty Subset of
I[01] st
(
Z = [.0,(TT . (len TT)).] &
Fn1 | [:{y},Z:] = Fn2 | [:{y},Z:] )
by A289;
hence
Fn1 | [:{y}, the carrier of I[01]:] = Fn2 | [:{y}, the carrier of I[01]:]
by A284, BORSUK_1:83;
verum
end;
for p being Point of [:Y,I[01]:]
for V being Subset of R^1 st G . p in V & V is open holds
ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V )
proof
let p be
Point of
[:Y,I[01]:];
for V being Subset of R^1 st G . p in V & V is open holds
ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V )let V be
Subset of
R^1;
( G . p in V & V is open implies ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V ) )
assume A397:
(
G . p in V &
V is
open )
;
ex W being Subset of [:Y,I[01]:] st
( p in W & W is open & G .: W c= V )
consider y being
Point of
Y,
t being
Point of
I[01],
N being non
empty open Subset of
Y,
Fn being
Function of
[:(Y | N),I[01]:],
R^1 such that A398:
p = [y,t]
and A399:
G . p = Fn . p
and A400:
y in N
and A401:
Fn is
continuous
and A402:
(
F | [:N, the carrier of I[01]:] = CircleMap * Fn &
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] )
and
for
H being
Function of
[:(Y | N),I[01]:],
R^1 st
H is
continuous &
F | [:N, the carrier of I[01]:] = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H
by A271;
A403: the
carrier of
[:(Y | N),I[01]:] =
[: the carrier of (Y | N), the carrier of I[01]:]
by BORSUK_1:def 5
.=
[:N, the carrier of I[01]:]
by PRE_TOPC:29
;
then
p in the
carrier of
[:(Y | N),I[01]:]
by A398, A400, ZFMISC_1:106;
then consider W being
Subset of
[:(Y | N),I[01]:] such that A404:
p in W
and A405:
W is
open
and A406:
Fn .: W c= V
by A397, A399, A401, JGRAPH_2:20;
A407:
dom Fn = [:N, the carrier of I[01]:]
by A403, FUNCT_2:def 1;
A408:
[#] (Y | N) = N
by PRE_TOPC:def 10;
then A409:
[#] [:(Y | N),I[01]:] = [:N,([#] I[01]):]
by BORSUK_3:1;
[:(Y | N),I[01]:] = [:Y,I[01]:] | [:N,([#] I[01]):]
by Lm7, BORSUK_3:26;
then consider C being
Subset of
[:Y,I[01]:] such that A410:
C is
open
and A411:
C /\ ([#] [:(Y | N),I[01]:]) = W
by A405, TOPS_2:32;
take WW =
C /\ [:N,([#] I[01]):];
( p in WW & WW is open & G .: WW c= V )
thus
p in WW
by A404, A411, A408, BORSUK_3:1;
( WW is open & G .: WW c= V )
[:N,([#] I[01]):] is
open
by BORSUK_1:46;
hence
WW is
open
by A410;
G .: WW c= V
let y be
set ;
TARSKI:def 3 ( not y in G .: WW or y in V )
assume
y in G .: WW
;
y in V
then consider x being
Point of
[:Y,I[01]:] such that A412:
x in WW
and A413:
y = G . x
by FUNCT_2:116;
consider y0 being
Point of
Y,
t0 being
Point of
I[01],
N0 being non
empty open Subset of
Y,
Fn0 being
Function of
[:(Y | N0),I[01]:],
R^1 such that A414:
x = [y0,t0]
and A415:
G . x = Fn0 . x
and A416:
(
y0 in N0 &
Fn0 is
continuous &
F | [:N0, the carrier of I[01]:] = CircleMap * Fn0 &
Fn0 | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] )
and
for
H being
Function of
[:(Y | N0),I[01]:],
R^1 st
H is
continuous &
F | [:N0, the carrier of I[01]:] = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft | [:N0, the carrier of I[01]:] holds
Fn0 = H
by A271;
x in [:N,([#] I[01]):]
by A412, XBOOLE_0:def 4;
then A417:
y0 in N
by A414, ZFMISC_1:106;
A418:
x in [:{y0}, the carrier of I[01]:]
by A414, ZFMISC_1:128;
then Fn . x =
(Fn | [:{y0}, the carrier of I[01]:]) . x
by FUNCT_1:72
.=
(Fn0 | [:{y0}, the carrier of I[01]:]) . x
by A273, A401, A402, A414, A416, A417
.=
Fn0 . x
by A418, FUNCT_1:72
;
then
y in Fn .: W
by A407, A411, A409, A412, A413, A415, FUNCT_1:def 12;
hence
y in V
by A406;
verum
end;
hence
G is continuous
by JGRAPH_2:20; ( 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 x being Point of [:Y,I[01]:] holds F . x = (CircleMap * G) . x
proof
let x be
Point of
[:Y,I[01]:];
F . x = (CircleMap * G) . x
consider y being
Point of
Y,
t being
Point of
I[01],
N being non
empty open Subset of
Y,
Fn being
Function of
[:(Y | N),I[01]:],
R^1 such that A419:
x = [y,t]
and A420:
G . x = Fn . x
and A421:
y in N
and
Fn is
continuous
and A422:
F | [:N, the carrier of I[01]:] = CircleMap * Fn
and
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:]
and
for
H being
Function of
[:(Y | N),I[01]:],
R^1 st
H is
continuous &
F | [:N, the carrier of I[01]:] = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H
by A271;
A423: the
carrier of
[:(Y | N),I[01]:] =
[: the carrier of (Y | N), the carrier of I[01]:]
by BORSUK_1:def 5
.=
[:N, the carrier of I[01]:]
by PRE_TOPC:29
;
then A424:
x in the
carrier of
[:(Y | N),I[01]:]
by A419, A421, ZFMISC_1:106;
thus (CircleMap * G) . x =
CircleMap . (G . x)
by FUNCT_2:21
.=
(CircleMap * Fn) . x
by A420, A424, FUNCT_2:21
.=
F . x
by A422, A423, A424, FUNCT_1:72
;
verum
end;
hence
F = CircleMap * G
by FUNCT_2:113; ( 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 ) )
A425:
[: the carrier of Y,{0}:] c= [: the carrier of Y, the carrier of I[01]:]
by Lm3, ZFMISC_1:118;
A426:
the carrier of [:Y,I[01]:] = [: the carrier of Y, the carrier of I[01]:]
by BORSUK_1:def 5;
then A427:
dom G = [: the carrier of Y, the carrier of I[01]:]
by FUNCT_2:def 1;
A428:
for x being set st x in dom Ft holds
Ft . x = G . x
proof
let x be
set ;
( x in dom Ft implies Ft . x = G . x )
assume A429:
x in dom Ft
;
Ft . x = G . x
then
x in dom G
by A8, A427, A425;
then consider y being
Point of
Y,
t being
Point of
I[01],
N being non
empty open Subset of
Y,
Fn being
Function of
[:(Y | N),I[01]:],
R^1 such that A430:
x = [y,t]
and A431:
G . x = Fn . x
and A432:
y in N
and
Fn is
continuous
and
F | [:N, the carrier of I[01]:] = CircleMap * Fn
and A433:
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:]
and
for
H being
Function of
[:(Y | N),I[01]:],
R^1 st
H is
continuous &
F | [:N, the carrier of I[01]:] = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H
by A271;
x in [:N, the carrier of I[01]:]
by A430, A432, ZFMISC_1:106;
hence Ft . x =
(Ft | [:N, the carrier of I[01]:]) . x
by FUNCT_1:72
.=
G . x
by A7, A429, A431, A433, Lm14, FUNCT_1:72
;
verum
end;
dom Ft = (dom G) /\ [: the carrier of Y,{0}:]
by A8, A427, A425, XBOOLE_1:28;
hence
G | [: the carrier of Y,{0}:] = Ft
by A428, FUNCT_1:68; 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 H be Function of [:Y,I[01]:],R^1; ( H is continuous & F = CircleMap * H & H | [: the carrier of Y,{0}:] = Ft implies G = H )
assume that
A434:
( H is continuous & F = CircleMap * H )
and
A435:
H | [: the carrier of Y,{0}:] = Ft
; G = H
for x being Point of [:Y,I[01]:] holds G . x = H . x
proof
let x be
Point of
[:Y,I[01]:];
G . x = H . x
consider y being
Point of
Y,
t being
Point of
I[01],
N being non
empty open Subset of
Y,
Fn being
Function of
[:(Y | N),I[01]:],
R^1 such that A436:
x = [y,t]
and A437:
G . x = Fn . x
and A438:
y in N
and
Fn is
continuous
and
F | [:N, the carrier of I[01]:] = CircleMap * Fn
and
Fn | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:]
and A439:
for
H being
Function of
[:(Y | N),I[01]:],
R^1 st
H is
continuous &
F | [:N, the carrier of I[01]:] = CircleMap * H &
H | [: the carrier of Y,{0}:] = Ft | [:N, the carrier of I[01]:] holds
Fn = H
by A271;
A440: the
carrier of
[:(Y | N),I[01]:] =
[: the carrier of (Y | N), the carrier of I[01]:]
by BORSUK_1:def 5
.=
[:N, the carrier of I[01]:]
by PRE_TOPC:29
;
then A441:
x in the
carrier of
[:(Y | N),I[01]:]
by A436, A438, ZFMISC_1:106;
dom H = the
carrier of
[:Y,I[01]:]
by FUNCT_2:def 1;
then
[:N, the carrier of I[01]:] c= dom H
by A426, ZFMISC_1:118;
then A442:
dom (H | [:N, the carrier of I[01]:]) = [:N, the carrier of I[01]:]
by RELAT_1:91;
rng (H | [:N, the carrier of I[01]:]) c= the
carrier of
R^1
;
then reconsider H1 =
H | [:N, the carrier of I[01]:] as
Function of
[:(Y | N),I[01]:],
R^1 by A440, A442, FUNCT_2:4;
A443:
(H | [:N, the carrier of I[01]:]) | [: the carrier of Y,{0}:] =
H | ([: the carrier of Y,{0}:] /\ [:N, the carrier of I[01]:])
by RELAT_1:100
.=
Ft | [:N, the carrier of I[01]:]
by A435, RELAT_1:100
;
(
H1 is
continuous &
F | [:N, the carrier of I[01]:] = CircleMap * (H | [:N, the carrier of I[01]:]) )
by A434, RELAT_1:112, TOPALG_3:18;
hence G . x =
(H | [:N, the carrier of I[01]:]) . x
by A437, A439, A443
.=
H . x
by A440, A441, FUNCT_1:72
;
verum
end;
hence
G = H
by FUNCT_2:113; verum