thus
Ciso is one-to-one
:: thesis: Ciso is onto

let q be object ; :: according to TARSKI:def 3 :: thesis: ( 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])) ; :: thesis: 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; :: thesis: verum

proof

thus
rng Ciso c= the carrier of (pi_1 ((Tunit_circle 2),c[10]))
; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: the carrier of (pi_1 ((Tunit_circle 2),c[10])) c= rng Ciso
set xt = R^1 0;

let m, n be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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);

.= 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);

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; :: thesis: verum

end;let m, n be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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);

A11: now :: thesis: for x being Point of I[01] holds (CircleMap * (Prj1 (j0,Ft))) . x = (cLoop m) . x

(Prj1 (j0,Ft)) . 0 =
Ft . (j0,j0)
by Def2
let x be Point of I[01]; :: thesis: (CircleMap * (Prj1 (j0,Ft))) . x = (cLoop m) . x

thus (CircleMap * (Prj1 (j0,Ft))) . x = CircleMap . ((Prj1 (j0,Ft)) . x) by FUNCT_2:15

.= CircleMap . (Ft . (x,j0)) by Def2

.= F . (x,j0) by A9, Lm5, BINOP_1:18

.= (cLoop m) . x by A5 ; :: thesis: verum

end;thus (CircleMap * (Prj1 (j0,Ft))) . x = CircleMap . ((Prj1 (j0,Ft)) . x) by FUNCT_2:15

.= CircleMap . (Ft . (x,j0)) by Def2

.= F . (x,j0) by A9, Lm5, BINOP_1:18

.= (cLoop m) . x by A5 ; :: thesis: verum

.= 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);

A13: now :: thesis: for x being Point of I[01] holds (CircleMap * (Prj1 (j1,Ft))) . x = (cLoop n) . x

consider ftn being Function of I[01],R^1 such that let x be Point of I[01]; :: thesis: (CircleMap * (Prj1 (j1,Ft))) . x = (cLoop n) . x

thus (CircleMap * (Prj1 (j1,Ft))) . x = CircleMap . ((Prj1 (j1,Ft)) . x) by FUNCT_2:15

.= CircleMap . (Ft . (x,j1)) by Def2

.= F . (x,j1) by A9, Lm5, BINOP_1:18

.= (cLoop n) . x by A5 ; :: thesis: verum

end;thus (CircleMap * (Prj1 (j1,Ft))) . x = CircleMap . ((Prj1 (j1,Ft)) . x) by FUNCT_2:15

.= CircleMap . (Ft . (x,j1)) by Def2

.= F . (x,j1) by A9, Lm5, BINOP_1:18

.= (cLoop n) . x by A5 ; :: thesis: verum

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; :: thesis: verum

let q be object ; :: according to TARSKI:def 3 :: thesis: ( 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])) ; :: thesis: 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; :: thesis: verum