thus
Ciso is one-to-one
Ciso is onto proof
set xt =
R^1 0 ;
let m,
n be
set ;
FUNCT_1:def 8 ( not m in proj1 Ciso or not n in proj1 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:47;
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] ) ) )
by BORSUK_2:def 7;
A6:
R^1 0 in CircleMap " {c[10] }
by Lm1, TOPREALB:34, 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 13;
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 13
;
then A12:
Prj1 j0,
Ft = ftm
by A7, A11, FUNCT_2:113;
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 13
;
then A16:
Prj1 j1,
Ft = ftn
by A14, A13, FUNCT_2:113;
(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 13
.=
Ft . j1,
j1
by A8, BORSUK_6:def 13
.=
(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= proj2 Ciso
let q be set ; TARSKI:def 3 ( not q in the carrier of (pi_1 (Tunit_circle 2),c[10] ) or q in proj2 Ciso )
assume
q in the carrier of (pi_1 (Tunit_circle 2),c[10] )
; q in proj2 Ciso
then consider f being Loop of c[10] such that
A19:
q = Class (EqRel (Tunit_circle 2),c[10] ),f
by TOPALG_1:48;
R^1 0 in CircleMap " {c[10] }
by Lm1, TOPREALB:34, 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;
CircleMap . (ft . j1) =
(CircleMap * ft) . j1
by FUNCT_2:21
.=
c[10]
by A21, BORSUK_2:def 4
;
then
CircleMap . (ft . 1) in {c[10] }
by TARSKI:def 1;
then A23:
ft . 1 in INT
by Lm12, FUNCT_1:def 13, TOPREALB:34;
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 A23, Th25, FUNCT_2:def 1;
hence
q in proj2 Ciso
by A19, A21, A23, FUNCT_1:def 5; verum