set Y = 1TopSp {1};
let x0, y0 be Point of (Tunit_circle 2); for xt being Point of R^1
for f being Path of x0,y0 st xt in CircleMap " {x0} holds
ex ft being Function of I[01],R^1 st
( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
let xt be Point of R^1; for f being Path of x0,y0 st xt in CircleMap " {x0} holds
ex ft being Function of I[01],R^1 st
( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
let f be Path of x0,y0; ( xt in CircleMap " {x0} implies ex ft being Function of I[01],R^1 st
( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) ) )
deffunc H1( set , Element of the carrier of I[01]) -> Element of the carrier of (Tunit_circle 2) = f . $2;
consider F being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of (Tunit_circle 2) such that
A1:
for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds F . (y,i) = H1(y,i)
from BINOP_1:sch 4();
reconsider j = 1 as Point of (1TopSp {1}) by TARSKI:def 1;
A2:
[j,j0] in [: the carrier of (1TopSp {1}),{0}:]
by Lm4, ZFMISC_1:87;
A3:
the carrier of [:(1TopSp {1}),I[01]:] = [: the carrier of (1TopSp {1}), the carrier of I[01]:]
by BORSUK_1:def 2;
then reconsider F = F as Function of [:(1TopSp {1}),I[01]:],(Tunit_circle 2) ;
set Ft = [:(1TopSp {1}),(Sspace 0[01]):] --> xt;
A4:
the carrier of [:(1TopSp {1}),(Sspace 0[01]):] = [: the carrier of (1TopSp {1}), the carrier of (Sspace 0[01]):]
by BORSUK_1:def 2;
then A5:
for y being Element of (1TopSp {1})
for i being Element of {0} holds ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [y,i] = xt
by Lm14, FUNCOP_1:7;
A6:
[#] (1TopSp {1}) = the carrier of (1TopSp {1})
;
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )
proof
let p be
Point of
[:(1TopSp {1}),I[01]:];
for V being Subset of (Tunit_circle 2) st F . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )let V be
Subset of
(Tunit_circle 2);
( F . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V ) )
assume A7:
(
F . p in V &
V is
open )
;
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & F .: W c= V )
consider p1 being
Point of
(1TopSp {1}),
p2 being
Point of
I[01] such that A8:
p = [p1,p2]
by BORSUK_1:10;
F . (
p1,
p2)
= f . p2
by A1;
then consider S being
Subset of
I[01] such that A9:
p2 in S
and A10:
S is
open
and A11:
f .: S c= V
by A7, A8, JGRAPH_2:10;
set W =
[:{1},S:];
[:{1},S:] c= [: the carrier of (1TopSp {1}), the carrier of I[01]:]
by ZFMISC_1:95;
then reconsider W =
[:{1},S:] as
Subset of
[:(1TopSp {1}),I[01]:] by BORSUK_1:def 2;
take
W
;
( p in W & W is open & F .: W c= V )
thus
p in W
by A8, A9, ZFMISC_1:87;
( W is open & F .: W c= V )
thus
W is
open
by A6, A10, BORSUK_1:6;
F .: W c= V
let y be
object ;
TARSKI:def 3 ( not y in F .: W or y in V )
assume
y in F .: W
;
y in V
then consider x being
object such that A12:
x in the
carrier of
[:(1TopSp {1}),I[01]:]
and A13:
x in W
and A14:
y = F . x
by FUNCT_2:64;
consider x1 being
Point of
(1TopSp {1}),
x2 being
Point of
I[01] such that A15:
x = [x1,x2]
by A12, BORSUK_1:10;
x2 in S
by A13, A15, ZFMISC_1:87;
then A16:
f . x2 in f .: S
by FUNCT_2:35;
y =
F . (
x1,
x2)
by A14, A15
.=
f . x2
by A1
;
hence
y in V
by A11, A16;
verum
end;
then A17:
F is continuous
by JGRAPH_2:10;
assume
xt in CircleMap " {x0}
; ex ft being Function of I[01],R^1 st
( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
then A18:
CircleMap . xt in {x0}
by FUNCT_2:38;
A19:
for x being object st x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) holds
(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x
proof
let x be
object ;
( x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) implies (F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x )
assume A20:
x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt))
;
(F | [: the carrier of (1TopSp {1}),{0}:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x
consider x1,
x2 being
object such that A21:
x1 in the
carrier of
(1TopSp {1})
and A22:
x2 in {0}
and A23:
x = [x1,x2]
by A4, A20, Lm14, ZFMISC_1:def 2;
A24:
x2 = 0
by A22, TARSKI:def 1;
thus (F | [: the carrier of (1TopSp {1}),{0}:]) . x =
F . (
x1,
x2)
by A4, A20, A23, Lm14, FUNCT_1:49
.=
f . x2
by A1, A21, A24, Lm2
.=
x0
by A24, BORSUK_2:def 4
.=
CircleMap . xt
by A18, TARSKI:def 1
.=
CircleMap . (([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x)
by A5, A21, A22, A23
.=
(CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) . x
by A20, FUNCT_1:12
;
verum
end;
A25:
dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01]):] --> xt)) = [: the carrier of (1TopSp {1}),{0}:]
by A4, Lm14, FUNCT_2:def 1;
A26:
dom F = the carrier of [:(1TopSp {1}),I[01]:]
by FUNCT_2:def 1;
then A27:
[: the carrier of (1TopSp {1}),{0}:] c= dom F
by A3, Lm3, ZFMISC_1:95;
then
dom (F | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:]
by RELAT_1:62;
then consider G being Function of [:(1TopSp {1}),I[01]:],R^1 such that
A28:
G is continuous
and
A29:
F = CircleMap * G
and
A30:
G | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt
and
A31:
for H being Function of [:(1TopSp {1}),I[01]:],R^1 st H is continuous & F = CircleMap * H & H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt holds
G = H
by A17, A25, A19, Th22, FUNCT_1:2;
take ft = Prj2 (j,G); ( ft . 0 = xt & f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
thus ft . 0 =
G . (j,j0)
by Def3
.=
([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . [j,j0]
by A30, A2, FUNCT_1:49
.=
xt
by A5, Lm4
; ( f = CircleMap * ft & ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
for i being Point of I[01] holds f . i = (CircleMap * ft) . i
hence
f = CircleMap * ft
; ( ft is continuous & ( for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1 ) )
thus
ft is continuous
by A28; for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt holds
ft = f1
let f1 be Function of I[01],R^1; ( f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt implies ft = f1 )
deffunc H2( set , Element of the carrier of I[01]) -> Element of the carrier of R^1 = f1 . $2;
consider H being Function of [: the carrier of (1TopSp {1}), the carrier of I[01]:], the carrier of R^1 such that
A33:
for y being Element of (1TopSp {1})
for i being Element of the carrier of I[01] holds H . (y,i) = H2(y,i)
from BINOP_1:sch 4();
reconsider H = H as Function of [:(1TopSp {1}),I[01]:],R^1 by A3;
assume that
A34:
f1 is continuous
and
A35:
f = CircleMap * f1
and
A36:
f1 . 0 = xt
; ft = f1
for p being Point of [:(1TopSp {1}),I[01]:]
for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )
proof
let p be
Point of
[:(1TopSp {1}),I[01]:];
for V being Subset of R^1 st H . p in V & V is open holds
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )let V be
Subset of
R^1;
( H . p in V & V is open implies ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V ) )
assume A37:
(
H . p in V &
V is
open )
;
ex W being Subset of [:(1TopSp {1}),I[01]:] st
( p in W & W is open & H .: W c= V )
consider p1 being
Point of
(1TopSp {1}),
p2 being
Point of
I[01] such that A38:
p = [p1,p2]
by BORSUK_1:10;
H . p =
H . (
p1,
p2)
by A38
.=
f1 . p2
by A33
;
then consider W being
Subset of
I[01] such that A39:
p2 in W
and A40:
W is
open
and A41:
f1 .: W c= V
by A34, A37, JGRAPH_2:10;
take W1 =
[:([#] (1TopSp {1})),W:];
( p in W1 & W1 is open & H .: W1 c= V )
thus
p in W1
by A38, A39, ZFMISC_1:87;
( W1 is open & H .: W1 c= V )
thus
W1 is
open
by A40, BORSUK_1:6;
H .: W1 c= V
let y be
object ;
TARSKI:def 3 ( not y in H .: W1 or y in V )
assume
y in H .: W1
;
y in V
then consider c being
Element of
[:(1TopSp {1}),I[01]:] such that A42:
c in W1
and A43:
y = H . c
by FUNCT_2:65;
consider c1,
c2 being
object such that A44:
c1 in [#] (1TopSp {1})
and A45:
c2 in W
and A46:
c = [c1,c2]
by A42, ZFMISC_1:def 2;
A47:
f1 . c2 in f1 .: W
by A45, FUNCT_2:35;
H . c =
H . (
c1,
c2)
by A46
.=
f1 . c2
by A33, A44, A45
;
hence
y in V
by A41, A43, A47;
verum
end;
then A48:
H is continuous
by JGRAPH_2:10;
for x being Point of [:(1TopSp {1}),I[01]:] holds F . x = (CircleMap * H) . x
then A50:
F = CircleMap * H
;
for i being Point of I[01] holds ft . i = f1 . i
proof
let i be
Point of
I[01];
ft . i = f1 . i
A51:
dom H = the
carrier of
[:(1TopSp {1}),I[01]:]
by FUNCT_2:def 1;
then A52:
dom (H | [: the carrier of (1TopSp {1}),{0}:]) = [: the carrier of (1TopSp {1}),{0}:]
by A26, A27, RELAT_1:62;
A53:
for
x being
object st
x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) holds
(H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x
proof
let x be
object ;
( x in dom (H | [: the carrier of (1TopSp {1}),{0}:]) implies (H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x )
assume A54:
x in dom (H | [: the carrier of (1TopSp {1}),{0}:])
;
(H | [: the carrier of (1TopSp {1}),{0}:]) . x = ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x
then consider x1,
x2 being
object such that A55:
x1 in the
carrier of
(1TopSp {1})
and A56:
x2 in {0}
and A57:
x = [x1,x2]
by A52, ZFMISC_1:def 2;
A58:
x2 = j0
by A56, TARSKI:def 1;
thus (H | [: the carrier of (1TopSp {1}),{0}:]) . x =
H . (
x1,
x2)
by A54, A57, FUNCT_1:47
.=
f1 . x2
by A33, A55, A58
.=
([:(1TopSp {1}),(Sspace 0[01]):] --> xt) . x
by A5, A36, A55, A56, A57, A58
;
verum
end;
dom ([:(1TopSp {1}),(Sspace 0[01]):] --> xt) = [: the carrier of (1TopSp {1}),{0}:]
by A4, Lm14, FUNCT_2:def 1;
then A59:
H | [: the carrier of (1TopSp {1}),{0}:] = [:(1TopSp {1}),(Sspace 0[01]):] --> xt
by A26, A27, A51, A53, RELAT_1:62;
thus ft . i =
G . (
j,
i)
by Def3
.=
H . (
j,
i)
by A31, A50, A48, A59
.=
f1 . i
by A33
;
verum
end;
hence
ft = f1
; verum