let x0, y0 be Point of (Tunit_circle 2); :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ) ) )
assume
xt in CircleMap " {x0}
; :: thesis: 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 A1:
CircleMap . xt in {x0}
by FUNCT_2:46;
set Y = 1TopSp {1};
A2:
[#] (1TopSp {1}) = the carrier of (1TopSp {1})
;
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
A3:
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();
A4:
the carrier of [:(1TopSp {1}),I[01] :] = [:the carrier of (1TopSp {1}),the carrier of I[01] :]
by BORSUK_1:def 5;
then reconsider F = F as Function of [:(1TopSp {1}),I[01] :],(Tunit_circle 2) ;
reconsider j = 1 as Point of (1TopSp {1}) by TARSKI:def 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] :];
:: thesis: 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);
:: thesis: ( 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 that A5:
F . p in V
and A6:
V is
open
;
:: thesis: 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 A7:
p = [p1,p2]
by BORSUK_1:50;
F . p1,
p2 = f . p2
by A3;
then consider S being
Subset of
I[01] such that A8:
p2 in S
and A9:
S is
open
and A10:
f .: S c= V
by A5, A6, A7, JGRAPH_2:20;
set W =
[:{1},S:];
[:{1},S:] c= [:the carrier of (1TopSp {1}),the carrier of I[01] :]
by ZFMISC_1:118;
then reconsider W =
[:{1},S:] as
Subset of
[:(1TopSp {1}),I[01] :] by BORSUK_1:def 5;
take
W
;
:: thesis: ( p in W & W is open & F .: W c= V )
thus
p in W
by A7, A8, ZFMISC_1:106;
:: thesis: ( W is open & F .: W c= V )
thus
W is
open
by A2, A9, BORSUK_1:46;
:: thesis: F .: W c= V
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in F .: W or y in V )
assume
y in F .: W
;
:: thesis: y in V
then consider x being
set such that A11:
x in the
carrier of
[:(1TopSp {1}),I[01] :]
and A12:
x in W
and A13:
y = F . x
by FUNCT_2:115;
consider x1 being
Point of
(1TopSp {1}),
x2 being
Point of
I[01] such that A14:
x = [x1,x2]
by A11, BORSUK_1:50;
A15:
y =
F . x1,
x2
by A13, A14
.=
f . x2
by A3
;
x2 in S
by A12, A14, ZFMISC_1:106;
then
f . x2 in f .: S
by FUNCT_2:43;
hence
y in V
by A10, A15;
:: thesis: verum
end;
then A16:
F is continuous
by JGRAPH_2:20;
A17:
dom F = the carrier of [:(1TopSp {1}),I[01] :]
by FUNCT_2:def 1;
then A18:
[:the carrier of (1TopSp {1}),{0 }:] c= dom F
by A4, Lm3, ZFMISC_1:118;
then A19:
dom (F | [:the carrier of (1TopSp {1}),{0 }:]) = [:the carrier of (1TopSp {1}),{0 }:]
by RELAT_1:91;
A20:
the carrier of [:(1TopSp {1}),(Sspace 0[01] ):] = [:the carrier of (1TopSp {1}),the carrier of (Sspace 0[01] ):]
by BORSUK_1:def 5;
set Ft = [:(1TopSp {1}),(Sspace 0[01] ):] --> xt;
A21:
dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt)) = [:the carrier of (1TopSp {1}),{0 }:]
by A20, Lm14, FUNCT_2:def 1;
A22:
for y being Element of (1TopSp {1})
for i being Element of {0 } holds ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) . [y,i] = xt
by A20, Lm14, FUNCOP_1:13;
for x being set 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
set ;
:: thesis: ( 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 A23:
x in dom (CircleMap * ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt))
;
:: thesis: (F | [:the carrier of (1TopSp {1}),{0 }:]) . x = (CircleMap * ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt)) . x
consider x1,
x2 being
set such that A24:
x1 in the
carrier of
(1TopSp {1})
and A25:
x2 in {0 }
and A26:
x = [x1,x2]
by A20, A23, Lm14, ZFMISC_1:def 2;
A27:
x2 = 0
by A25, TARSKI:def 1;
thus (F | [:the carrier of (1TopSp {1}),{0 }:]) . x =
F . x1,
x2
by A20, A23, A26, Lm14, FUNCT_1:72
.=
f . x2
by A3, A24, A27, Lm2
.=
x0
by A27, BORSUK_2:def 4
.=
CircleMap . xt
by A1, TARSKI:def 1
.=
CircleMap . (([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) . x)
by A22, A24, A25, A26
.=
(CircleMap * ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt)) . x
by A23, FUNCT_1:22
;
:: thesis: verum
end;
then
F | [:the carrier of (1TopSp {1}),{0 }:] = CircleMap * ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt)
by A19, A21, FUNCT_1:9;
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 A16, Th22;
take ft = Prj2 j,G; :: thesis: ( 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 ) )
A32:
[j,j0] in [:the carrier of (1TopSp {1}),{0 }:]
by Lm4, ZFMISC_1:106;
thus ft . 0 =
G . j,j0
by Def3
.=
([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) . [j,j0]
by A30, A32, FUNCT_1:72
.=
xt
by A22, Lm4
; :: thesis: ( 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
by FUNCT_2:113; :: thesis: ( 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; :: thesis: 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 ; :: thesis: ( f1 is continuous & f = CircleMap * f1 & f1 . 0 = xt implies ft = f1 )
assume that
A34:
f1 is continuous
and
A35:
f = CircleMap * f1
and
A36:
f1 . 0 = xt
; :: thesis: 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
A37:
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 A4;
for x being Point of [:(1TopSp {1}),I[01] :] holds F . x = (CircleMap * H) . x
then A39:
F = CircleMap * H
by FUNCT_2:113;
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] :];
:: thesis: 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 ;
:: thesis: ( 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 that A40:
H . p in V
and A41:
V is
open
;
:: thesis: 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 A42:
p = [p1,p2]
by BORSUK_1:50;
H . p =
H . p1,
p2
by A42
.=
f1 . p2
by A37
;
then consider W being
Subset of
I[01] such that A43:
p2 in W
and A44:
W is
open
and A45:
f1 .: W c= V
by A34, A40, A41, JGRAPH_2:20;
take W1 =
[:([#] (1TopSp {1})),W:];
:: thesis: ( p in W1 & W1 is open & H .: W1 c= V )
thus
p in W1
by A42, A43, ZFMISC_1:106;
:: thesis: ( W1 is open & H .: W1 c= V )
thus
W1 is
open
by A44, BORSUK_1:46;
:: thesis: H .: W1 c= V
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in H .: W1 or y in V )
assume
y in H .: W1
;
:: thesis: y in V
then consider c being
Element of
[:(1TopSp {1}),I[01] :] such that A46:
c in W1
and A47:
y = H . c
by FUNCT_2:116;
consider c1,
c2 being
set such that A48:
c1 in [#] (1TopSp {1})
and A49:
c2 in W
and A50:
c = [c1,c2]
by A46, ZFMISC_1:def 2;
A51:
H . c =
H . c1,
c2
by A50
.=
f1 . c2
by A37, A48, A49
;
f1 . c2 in f1 .: W
by A49, FUNCT_2:43;
hence
y in V
by A45, A47, A51;
:: thesis: verum
end;
then A52:
H is continuous
by JGRAPH_2:20;
for i being Point of I[01] holds ft . i = f1 . i
proof
let i be
Point of
I[01] ;
:: thesis: ft . i = f1 . i
dom H = the
carrier of
[:(1TopSp {1}),I[01] :]
by FUNCT_2:def 1;
then A53:
dom (H | [:the carrier of (1TopSp {1}),{0 }:]) = [:the carrier of (1TopSp {1}),{0 }:]
by A17, A18, RELAT_1:91;
A54:
dom ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) = [:the carrier of (1TopSp {1}),{0 }:]
by A20, Lm14, FUNCT_2:def 1;
for
x being
set 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
set ;
:: thesis: ( 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 A55:
x in dom (H | [:the carrier of (1TopSp {1}),{0 }:])
;
:: thesis: (H | [:the carrier of (1TopSp {1}),{0 }:]) . x = ([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) . x
then consider x1,
x2 being
set such that A56:
x1 in the
carrier of
(1TopSp {1})
and A57:
x2 in {0 }
and A58:
x = [x1,x2]
by A53, ZFMISC_1:def 2;
A59:
x2 = j0
by A57, TARSKI:def 1;
thus (H | [:the carrier of (1TopSp {1}),{0 }:]) . x =
H . x1,
x2
by A55, A58, FUNCT_1:70
.=
f1 . x2
by A37, A56, A59
.=
([:(1TopSp {1}),(Sspace 0[01] ):] --> xt) . x
by A22, A36, A56, A57, A58, A59
;
:: thesis: verum
end;
then A60:
H | [:the carrier of (1TopSp {1}),{0 }:] = [:(1TopSp {1}),(Sspace 0[01] ):] --> xt
by A53, A54, FUNCT_1:9;
thus ft . i =
G . j,
i
by Def3
.=
H . j,
i
by A31, A39, A52, A60
.=
f1 . i
by A37
;
:: thesis: verum
end;
hence
ft = f1
by FUNCT_2:113; :: thesis: verum