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