thus
Ciso is one-to-one
Ciso is onto proof
set xt =
R^1 0;
let m,
n be
object ;
FUNCT_1:def 4 ( not m in dom Ciso or not n in dom Ciso or not Ciso . m = Ciso . n or m = n )
assume that A1:
(
m in dom Ciso &
n in dom Ciso )
and A2:
Ciso . m = Ciso . n
;
m = n
reconsider m =
m,
n =
n as
Integer by A1;
(
Ciso . m = Class (
(EqRel ((Tunit_circle 2),c[10])),
(cLoop m)) &
Ciso . n = Class (
(EqRel ((Tunit_circle 2),c[10])),
(cLoop n)) )
by Def5;
then A3:
cLoop m,
cLoop n are_homotopic
by A2, TOPALG_1:46;
then consider F being
Function of
[:I[01],I[01]:],
(Tunit_circle 2) such that A4:
F is
continuous
and A5:
for
s being
Point of
I[01] holds
(
F . (
s,
0)
= (cLoop m) . s &
F . (
s,1)
= (cLoop n) . s & ( for
t being
Point of
I[01] holds
(
F . (
0,
t)
= c[10] &
F . (1,
t)
= c[10] ) ) )
;
A6:
R^1 0 in CircleMap " {c[10]}
by Lm1, TOPREALB:33, TOPREALB:def 2;
then consider ftm being
Function of
I[01],
R^1 such that
ftm . 0 = R^1 0
and
cLoop m = CircleMap * ftm
and
ftm is
continuous
and A7:
for
f1 being
Function of
I[01],
R^1 st
f1 is
continuous &
cLoop m = CircleMap * f1 &
f1 . 0 = R^1 0 holds
ftm = f1
by Th23;
F is
Homotopy of
cLoop m,
cLoop n
by A3, A4, A5, BORSUK_6:def 11;
then consider yt being
Point of
R^1,
Pt,
Qt being
Path of
R^1 0,
yt,
Ft being
Homotopy of
Pt,
Qt such that A8:
Pt,
Qt are_homotopic
and A9:
F = CircleMap * Ft
and
yt in CircleMap " {c[10]}
and
for
F1 being
Homotopy of
Pt,
Qt st
F = CircleMap * F1 holds
Ft = F1
by A3, A6, Th24;
A10:
cLoop n = CircleMap * (ExtendInt n)
by Th20;
set ft0 =
Prj1 (
j0,
Ft);
(Prj1 (j0,Ft)) . 0 =
Ft . (
j0,
j0)
by Def2
.=
R^1 0
by A8, BORSUK_6:def 11
;
then A12:
Prj1 (
j0,
Ft)
= ftm
by A7, A11, FUNCT_2:63;
set ft1 =
Prj1 (
j1,
Ft);
consider ftn being
Function of
I[01],
R^1 such that
ftn . 0 = R^1 0
and
cLoop n = CircleMap * ftn
and
ftn is
continuous
and A14:
for
f1 being
Function of
I[01],
R^1 st
f1 is
continuous &
cLoop n = CircleMap * f1 &
f1 . 0 = R^1 0 holds
ftn = f1
by A6, Th23;
A15:
cLoop m = CircleMap * (ExtendInt m)
by Th20;
(Prj1 (j1,Ft)) . 0 =
Ft . (
j0,
j1)
by Def2
.=
R^1 0
by A8, BORSUK_6:def 11
;
then A16:
Prj1 (
j1,
Ft)
= ftn
by A14, A13, FUNCT_2:63;
(ExtendInt n) . 0 =
n * j0
by Def1
.=
R^1 0
by TOPREALB:def 2
;
then
ExtendInt n = ftn
by A14, A10;
then A17:
(Prj1 (j1,Ft)) . j1 = n * 1
by A16, Def1;
(ExtendInt m) . 0 =
m * j0
by Def1
.=
R^1 0
by TOPREALB:def 2
;
then
ExtendInt m = ftm
by A7, A15;
then A18:
(Prj1 (j0,Ft)) . j1 = m * 1
by A12, Def1;
(Prj1 (j0,Ft)) . j1 =
Ft . (
j1,
j0)
by Def2
.=
yt
by A8, BORSUK_6:def 11
.=
Ft . (
j1,
j1)
by A8, BORSUK_6:def 11
.=
(Prj1 (j1,Ft)) . j1
by Def2
;
hence
m = n
by A18, A17;
verum
end;
thus
rng Ciso c= the carrier of (pi_1 ((Tunit_circle 2),c[10]))
; FUNCT_2:def 3,XBOOLE_0:def 10 the carrier of (pi_1 ((Tunit_circle 2),c[10])) c= rng Ciso
let q be object ; TARSKI:def 3 ( not q in the carrier of (pi_1 ((Tunit_circle 2),c[10])) or q in rng Ciso )
assume
q in the carrier of (pi_1 ((Tunit_circle 2),c[10]))
; q in rng Ciso
then consider f being Loop of c[10] such that
A19:
q = Class ((EqRel ((Tunit_circle 2),c[10])),f)
by TOPALG_1:47;
R^1 0 in CircleMap " {c[10]}
by Lm1, TOPREALB:33, TOPREALB:def 2;
then consider ft being Function of I[01],R^1 such that
A20:
ft . 0 = R^1 0
and
A21:
f = CircleMap * ft
and
A22:
ft is continuous
and
for f1 being Function of I[01],R^1 st f1 is continuous & f = CircleMap * f1 & f1 . 0 = R^1 0 holds
ft = f1
by Th23;
A23:
ft . 1 in REAL
by XREAL_0:def 1;
CircleMap . (ft . j1) =
(CircleMap * ft) . j1
by FUNCT_2:15
.=
c[10]
by A21, BORSUK_2:def 4
;
then
CircleMap . (ft . 1) in {c[10]}
by TARSKI:def 1;
then A24:
ft . 1 in INT
by Lm12, FUNCT_1:def 7, TOPREALB:33, A23;
ft . 1 = R^1 (ft . 1)
by TOPREALB:def 2;
then
ft is Path of R^1 0, R^1 (ft . 1)
by A20, A22, BORSUK_2:def 4;
then
( dom Ciso = INT & Ciso . (ft . 1) = Class ((EqRel ((Tunit_circle 2),c[10])),(CircleMap * ft)) )
by A24, Th25, FUNCT_2:def 1;
hence
q in rng Ciso
by A19, A21, A24, FUNCT_1:def 3; verum