thus Ciso is one-to-one :: thesis: Ciso is onto
proof
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 ((),c[10])),()) & Ciso . n = Class ((EqRel ((),c[10])),()) ) by Def5;
then A3: cLoop m, cLoop n are_homotopic by ;
then consider F being Function of ,() such that
A4: F is continuous and
A5: for s being Point of I[01] holds
( F . (s,0) = () . s & F . (s,1) = () . 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 " by ;
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 ;
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 " and
for F1 being Homotopy of Pt,Qt st F = CircleMap * F1 holds
Ft = F1 by A3, A6, Th24;
A10: cLoop n = CircleMap * () by Th20;
set ft0 = Prj1 (j0,Ft);
A11: now :: thesis: for x being Point of I[01] holds (CircleMap * (Prj1 (j0,Ft))) . x = () . x
let x be Point of I[01]; :: thesis: (CircleMap * (Prj1 (j0,Ft))) . x = () . 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
.= () . x by A5 ; :: thesis: verum
end;
(Prj1 (j0,Ft)) . 0 = Ft . (j0,j0) by Def2
.= R^1 0 by ;
then A12: Prj1 (j0,Ft) = ftm by ;
set ft1 = Prj1 (j1,Ft);
A13: now :: thesis: for x being Point of I[01] holds (CircleMap * (Prj1 (j1,Ft))) . x = () . x
let x be Point of I[01]; :: thesis: (CircleMap * (Prj1 (j1,Ft))) . x = () . 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
.= () . x by A5 ; :: thesis: verum
end;
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 ;
A15: cLoop m = CircleMap * () by Th20;
(Prj1 (j1,Ft)) . 0 = Ft . (j0,j1) by Def2
.= R^1 0 by ;
then A16: Prj1 (j1,Ft) = ftn by ;
() . 0 = n * j0 by Def1
.= R^1 0 by TOPREALB:def 2 ;
then ExtendInt n = ftn by ;
then A17: (Prj1 (j1,Ft)) . j1 = n * 1 by ;
() . 0 = m * j0 by Def1
.= R^1 0 by TOPREALB:def 2 ;
then ExtendInt m = ftm by ;
then A18: (Prj1 (j0,Ft)) . j1 = m * 1 by ;
(Prj1 (j0,Ft)) . j1 = Ft . (j1,j0) by Def2
.= yt by
.= Ft . (j1,j1) by
.= (Prj1 (j1,Ft)) . j1 by Def2 ;
hence m = n by ; :: thesis: verum
end;
thus rng Ciso c= the carrier of (pi_1 ((),c[10])) ; :: according to FUNCT_2:def 3,XBOOLE_0:def 10 :: thesis: the carrier of (pi_1 ((),c[10])) c= rng Ciso
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in the carrier of (pi_1 ((),c[10])) or q in rng Ciso )
assume q in the carrier of (pi_1 ((),c[10])) ; :: thesis:
then consider f being Loop of c[10] such that
A19: q = Class ((EqRel ((),c[10])),f) by TOPALG_1:47;
R^1 0 in CircleMap " by ;
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) = () . j1 by FUNCT_2:15
.= c[10] by ;
then CircleMap . (ft . 1) in by TARSKI:def 1;
then A24: ft . 1 in INT by ;
ft . 1 = R^1 (ft . 1) by TOPREALB:def 2;
then ft is Path of R^1 0, R^1 (ft . 1) by ;
then ( dom Ciso = INT & Ciso . (ft . 1) = Class ((EqRel ((),c[10])),()) ) by ;
hence q in rng Ciso by ; :: thesis: verum