A1: dom Ciso = INT by FUNCT_2:def 1;
thus Ciso is one-to-one :: thesis: Ciso is onto

proof

let m, n be set ; :: according to FUNCT_1:def 8 :: thesis: ( not m in dom Ciso or not n in dom Ciso or not Ciso . m = Ciso . n or m = n )
assume that
A2: ( m in dom Ciso & n in dom Ciso ) and
A3: Ciso . m = Ciso . n ; :: thesis: m = n
reconsider m = m, n = n as Integer by A2;
( 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 A4: cLoop m, cLoop n are_homotopic by A3, TOPALG_1:47;
then consider F being Function of [:I[01] ,I[01] :],(Tunit_circle 2) such that
A5: F is continuous and
A6: 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;
A7: F is Homotopy of cLoop m, cLoop n by A4, A5, A6, BORSUK_6:def 13;
set xt = R^1 0 ;
A8: R^1 0 in CircleMap " {c[10] } by Lm1, TOPREALB:34, TOPREALB:def 2;
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
A9: Pt,Qt are_homotopic and
A10: 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 A4, A7, Th24;
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
A11: 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 A8, Th23;
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
A12: 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 A8, Th23;
set ft0 = Prj1 j0,Ft;
set ft1 = Prj1 j1,Ft;
A13: (ExtendInt m) . 0 = m * j0 by Def1
.= R^1 0 by TOPREALB:def 2 ;
A14: (Prj1 j0,Ft) . 0 = Ft . j0,j0 by Def2
.= R^1 0 by A9, BORSUK_6:def 13 ;
cLoop m = CircleMap * (ExtendInt m) by Th20;
then A15: ExtendInt m = ftm by A11, A13;

now

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:21
.= CircleMap . (Ft . x,j0) by Def2
.= F . x,j0 by A10, Lm5, BINOP_1:30
.= (cLoop m) . x by A6 ; :: thesis: verum

end;

then cLoop m = CircleMap * (Prj1 j0,Ft) by FUNCT_2:113;
then Prj1 j0,Ft = ftm by A11, A14;
then A16: (Prj1 j0,Ft) . j1 = m * 1 by A15, Def1;
A17: (ExtendInt n) . 0 = n * j0 by Def1
.= R^1 0 by TOPREALB:def 2 ;
cLoop n = CircleMap * (ExtendInt n) by Th20;
then A18: ExtendInt n = ftn by A12, A17;
A19: (Prj1 j1,Ft) . 0 = Ft . j0,j1 by Def2
.= R^1 0 by A9, BORSUK_6:def 13 ;

now

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:21
.= CircleMap . (Ft . x,j1) by Def2
.= F . x,j1 by A10, Lm5, BINOP_1:30
.= (cLoop n) . x by A6 ; :: thesis: verum

end;

then cLoop n = CircleMap * (Prj1 j1,Ft) by FUNCT_2:113;
then Prj1 j1,Ft = ftn by A12, A19;
then A20: (Prj1 j1,Ft) . j1 = n * 1 by A18, Def1;
(Prj1 j0,Ft) . j1 = Ft . j1,j0 by Def2
.= yt by A9, BORSUK_6:def 13
.= Ft . j1,j1 by A9, BORSUK_6:def 13
.= (Prj1 j1,Ft) . j1 by Def2 ;
hence m = n by A16, A20; :: thesis: verum

end;

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
let q be set ; :: 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
A21: 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
A22: ft . 0 = R^1 0 and
A23: f = CircleMap * ft and
A24: 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 A23, BORSUK_2:def 4 ;
then CircleMap . (ft . 1) in {c[10] } by TARSKI:def 1;
then A25: ft . 1 in INT by Lm12, FUNCT_1:def 13, TOPREALB:34;
then A26: ft . 1 is Integer ;
ft is Path of R^1 0 , R^1 (ft . 1)

proof

thus ft is continuous by A24; :: according to BORSUK_2:def 4 :: thesis: ( ft . 0 = R^1 0 & ft . 1 = R^1 (ft . 1) )
thus ft . 0 = R^1 0 by A22; :: thesis: ft . 1 = R^1 (ft . 1)
thus ft . 1 = R^1 (ft . 1) by TOPREALB:def 2; :: thesis: verum

end;

then Ciso . (ft . 1) = Class (EqRel (Tunit_circle 2),c[10] ),(CircleMap * ft) by A26, Th25;
hence q in rng Ciso by A1, A21, A23, A25, FUNCT_1:def 5; :: thesis: verum