:: The Fundamental Group
:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users


theorem :: TOPALG_1:1
for G, H being set
for g being Function of G,H
for h being Function of H,G st h * g = id G & g * h = id H holds
h is bijective by FUNCT_2:23;

theorem Th2: :: TOPALG_1:2
for X being Subset of I[01]
for a being Point of I[01] st X = ].a,1.] holds
X ` = [.0,a.]
proof end;

theorem Th3: :: TOPALG_1:3
for X being Subset of I[01]
for a being Point of I[01] st X = [.0,a.[ holds
X ` = [.a,1.]
proof end;

theorem Th4: :: TOPALG_1:4
for X being Subset of I[01]
for a being Point of I[01] st X = ].a,1.] holds
X is open
proof end;

theorem Th5: :: TOPALG_1:5
for X being Subset of I[01]
for a being Point of I[01] st X = [.0,a.[ holds
X is open
proof end;

theorem :: TOPALG_1:6
for x being Real
for f being real-valued FinSequence holds x * (- f) = - (x * f)
proof end;

theorem Th7: :: TOPALG_1:7
for x being Real
for f, g being real-valued FinSequence holds x * (f - g) = (x * f) - (x * g) by RFUNCT_1:18;

theorem Th8: :: TOPALG_1:8
for x, y being Real
for f being real-valued FinSequence holds (x - y) * f = (x * f) - (y * f)
proof end;

theorem Th9: :: TOPALG_1:9
for f, g, h, k being real-valued FinSequence holds (f + g) - (h + k) = (f - h) + (g - k)
proof end;

theorem Th10: :: TOPALG_1:10
for x being Real
for n being Nat
for f being Element of REAL n st 0 <= x & x <= 1 holds
|.(x * f).| <= |.f.|
proof end;

theorem :: TOPALG_1:11
for n being Nat
for f being Element of REAL n
for p being Point of I[01] holds |.(p * f).| <= |.f.|
proof end;

theorem :: TOPALG_1:12
for x, y being Real
for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1 + p3 & e6 = p2 + p4 & dist (e1,e2) < x & dist (e3,e4) < y holds
dist (e5,e6) < x + y
proof end;

theorem Th13: :: TOPALG_1:13
for x, y being Real
for n being Nat
for e1, e2, e5, e6 being Point of (Euclid n)
for p1, p2 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = y * p1 & e6 = y * p2 & dist (e1,e2) < x & y <> 0 holds
dist (e5,e6) < |.y.| * x
proof end;

theorem Th14: :: TOPALG_1:14
for p, q, x, y being Real
for n being Nat
for e1, e2, e3, e4, e5, e6 being Point of (Euclid n)
for p1, p2, p3, p4 being Point of (TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (x * p1) + (y * p3) & e6 = (x * p2) + (y * p4) & dist (e1,e2) < p & dist (e3,e4) < q & x <> 0 & y <> 0 holds
dist (e5,e6) < (|.x.| * p) + (|.y.| * q)
proof end;

Lm1: for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (f1 . p) + (f2 . p) ) holds
g is continuous
proof end;

theorem Th15: :: TOPALG_1:15
for y being Real
for n being Nat
for X being non empty TopSpace
for f, g being Function of X,(TOP-REAL n) st f is continuous & ( for p being Point of X holds g . p = y * (f . p) ) holds
g is continuous
proof end;

theorem :: TOPALG_1:16
for x, y being Real
for n being Nat
for X being non empty TopSpace
for f1, f2, g being Function of X,(TOP-REAL n) st f1 is continuous & f2 is continuous & ( for p being Point of X holds g . p = (x * (f1 . p)) + (y * (f2 . p)) ) holds
g is continuous
proof end;

theorem Th17: :: TOPALG_1:17
for n being Nat
for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = (1 - i) * x ) holds
F is continuous
proof end;

theorem Th18: :: TOPALG_1:18
for n being Nat
for F being Function of [:(TOP-REAL n),I[01]:],(TOP-REAL n) st ( for x being Point of (TOP-REAL n)
for i being Point of I[01] holds F . (x,i) = i * x ) holds
F is continuous
proof end;

theorem Th19: :: TOPALG_1:19
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & b,c are_connected holds
for A1, A2 being Path of a,b
for B being Path of b,c st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic
proof end;

theorem :: TOPALG_1:20
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of b1,c1 st A1,A2 are_homotopic holds
A1,(A2 + B) + (- B) are_homotopic
proof end;

theorem Th21: :: TOPALG_1:21
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A1, A2 being Path of a,b
for B being Path of c,b st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
proof end;

theorem :: TOPALG_1:22
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of c1,b1 st A1,A2 are_homotopic holds
A1,(A2 + (- B)) + B are_homotopic
proof end;

theorem Th23: :: TOPALG_1:23
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,a are_connected holds
for A1, A2 being Path of a,b
for B being Path of c,a st A1,A2 are_homotopic holds
A1,((- B) + B) + A2 are_homotopic
proof end;

theorem :: TOPALG_1:24
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of c1,a1 st A1,A2 are_homotopic holds
A1,((- B) + B) + A2 are_homotopic
proof end;

theorem Th25: :: TOPALG_1:25
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & a,c are_connected holds
for A1, A2 being Path of a,b
for B being Path of a,c st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic
proof end;

theorem :: TOPALG_1:26
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A1, A2 being Path of a1,b1
for B being Path of a1,c1 st A1,A2 are_homotopic holds
A1,(B + (- B)) + A2 are_homotopic
proof end;

theorem Th27: :: TOPALG_1:27
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & c,b are_connected holds
for A, B being Path of a,b
for C being Path of b,c st A + C,B + C are_homotopic holds
A,B are_homotopic
proof end;

theorem :: TOPALG_1:28
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A, B being Path of a1,b1
for C being Path of b1,c1 st A + C,B + C are_homotopic holds
A,B are_homotopic
proof end;

theorem Th29: :: TOPALG_1:29
for X being non empty TopSpace
for a, b, c being Point of X st a,b are_connected & a,c are_connected holds
for A, B being Path of a,b
for C being Path of c,a st C + A,C + B are_homotopic holds
A,B are_homotopic
proof end;

theorem :: TOPALG_1:30
for T being non empty pathwise_connected TopSpace
for a1, b1, c1 being Point of T
for A, B being Path of a1,b1
for C being Path of c1,a1 st C + A,C + B are_homotopic holds
A,B are_homotopic
proof end;

theorem Th31: :: TOPALG_1:31
for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
proof end;

theorem :: TOPALG_1:32
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds ((A + B) + C) + D,(A + (B + C)) + D are_homotopic
proof end;

theorem Th33: :: TOPALG_1:33
for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
proof end;

theorem :: TOPALG_1:34
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds ((A + B) + C) + D,A + ((B + C) + D) are_homotopic
proof end;

theorem Th35: :: TOPALG_1:35
for X being non empty TopSpace
for a, b, c, d, e being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic
proof end;

theorem :: TOPALG_1:36
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1 holds (A + (B + C)) + D,(A + B) + (C + D) are_homotopic
proof end;

theorem Th37: :: TOPALG_1:37
for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & b,c are_connected & b,d are_connected holds
for A being Path of a,b
for B being Path of d,b
for C being Path of b,c holds ((A + (- B)) + B) + C,A + C are_homotopic
proof end;

theorem :: TOPALG_1:38
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 being Point of T
for A being Path of a1,b1
for B being Path of d1,b1
for C being Path of b1,c1 holds ((A + (- B)) + B) + C,A + C are_homotopic
proof end;

theorem Th39: :: TOPALG_1:39
for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & c,d are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
proof end;

theorem :: TOPALG_1:40
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 being Point of T
for A being Path of a1,b1
for B being Path of c1,d1
for C being Path of a1,c1 holds (((A + (- A)) + C) + B) + (- B),C are_homotopic
proof end;

theorem Th41: :: TOPALG_1:41
for X being non empty TopSpace
for a, b, c, d being Point of X st a,b are_connected & a,c are_connected & d,c are_connected holds
for A being Path of a,b
for B being Path of c,d
for C being Path of a,c holds (A + (((- A) + C) + B)) + (- B),C are_homotopic
proof end;

theorem :: TOPALG_1:42
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1 being Point of T
for A being Path of a1,b1
for B being Path of c1,d1
for C being Path of a1,c1 holds (A + (((- A) + C) + B)) + (- B),C are_homotopic
proof end;

theorem Th43: :: TOPALG_1:43
for X being non empty TopSpace
for a, b, c, d, e, f being Point of X st a,b are_connected & b,c are_connected & c,d are_connected & d,e are_connected & a,f are_connected holds
for A being Path of a,b
for B being Path of b,c
for C being Path of c,d
for D being Path of d,e
for E being Path of f,c holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
proof end;

theorem :: TOPALG_1:44
for T being non empty pathwise_connected TopSpace
for a1, b1, c1, d1, e1, f1 being Point of T
for A being Path of a1,b1
for B being Path of b1,c1
for C being Path of c1,d1
for D being Path of d1,e1
for E being Path of f1,c1 holds (A + (B + C)) + D,((A + B) + (- E)) + ((E + C) + D) are_homotopic
proof end;

definition
let T be TopStruct ;
let t be Point of T;
mode Loop of t is Path of t,t;
end;

definition
let T be non empty TopStruct ;
let t1, t2 be Point of T;
defpred S1[ object ] means $1 is Path of t1,t2;
func Paths (t1,t2) -> set means :Def1: :: TOPALG_1:def 1
 for x being object holds
( x in it iff x is Path of t1,t2 );
existence
ex b1 being set st
for x being object holds
( x in b1 iff x is Path of t1,t2 )
proof end;
uniqueness
for b1, b2 being set st ( for x being object holds
( x in b1 iff x is Path of t1,t2 ) ) & ( for x being object holds
( x in b2 iff x is Path of t1,t2 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Paths TOPALG_1:def 1 :
for T being non empty TopStruct
for t1, t2 being Point of T
for b4 being set holds
( b4 = Paths (t1,t2) iff for x being object holds
( x in b4 iff x is Path of t1,t2 ) );

registration
let T be non empty TopStruct ;
let t1, t2 be Point of T;
cluster Paths (t1,t2) -> non empty ;
coherence
not Paths (t1,t2) is empty
proof end;
end;

definition
let T be non empty TopStruct ;
let t be Point of T;
func Loops t -> set equals :: TOPALG_1:def 2
 Paths (t,t);
coherence
Paths (t,t) is set ;
end;

:: deftheorem defines Loops TOPALG_1:def 2 :
for T being non empty TopStruct
for t being Point of T holds Loops t = Paths (t,t);

registration
let T be non empty TopStruct ;
let t be Point of T;
cluster Loops t -> non empty ;
coherence
not Loops t is empty ;
end;

Lm2: for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
ex E being Equivalence_Relation of (Paths (a,b)) st
for x, y being object holds
( [x,y] in E iff ( x in Paths (a,b) & y in Paths (a,b) & ex P, Q being Path of a,b st
( P = x & Q = y & P,Q are_homotopic ) ) )
proof end;

definition
let X be non empty TopSpace;
let a, b be Point of X;
assume A1: a,b are_connected ;
func EqRel (X,a,b) -> Relation of (Paths (a,b)) means :Def3: :: TOPALG_1:def 3
 for P, Q being Path of a,b holds
( [P,Q] in it iff P,Q are_homotopic );
existence
ex b1 being Relation of (Paths (a,b)) st
for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic )
proof end;
uniqueness
for b1, b2 being Relation of (Paths (a,b)) st ( for P, Q being Path of a,b holds
( [P,Q] in b1 iff P,Q are_homotopic ) ) & ( for P, Q being Path of a,b holds
( [P,Q] in b2 iff P,Q are_homotopic ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines EqRel TOPALG_1:def 3 :
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for b4 being Relation of (Paths (a,b)) holds
( b4 = EqRel (X,a,b) iff for P, Q being Path of a,b holds
( [P,Q] in b4 iff P,Q are_homotopic ) );

Lm3: for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive )
proof end;

theorem Th45: :: TOPALG_1:45
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Q in Class ((EqRel (X,a,b)),P) iff P,Q are_homotopic )
proof end;

theorem Th46: :: TOPALG_1:46
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
for P, Q being Path of a,b holds
( Class ((EqRel (X,a,b)),P) = Class ((EqRel (X,a,b)),Q) iff P,Q are_homotopic )
proof end;

definition
let X be non empty TopSpace;
let a be Point of X;
func EqRel (X,a) -> Relation of (Loops a) equals :: TOPALG_1:def 4
 EqRel (X,a,a);
coherence
EqRel (X,a,a) is Relation of (Loops a) ;
end;

:: deftheorem defines EqRel TOPALG_1:def 4 :
for X being non empty TopSpace
for a being Point of X holds EqRel (X,a) = EqRel (X,a,a);

registration
let X be non empty TopSpace;
let a be Point of X;
cluster EqRel (X,a) -> non empty total symmetric transitive ;
coherence
( not EqRel (X,a) is empty & EqRel (X,a) is total & EqRel (X,a) is symmetric & EqRel (X,a) is transitive ) by Lm3;
end;

definition
let X be non empty TopSpace;
let a be Point of X;
set E = EqRel (X,a);
set A = Class (EqRel (X,a));
set W = Loops a;
func FundamentalGroup (X,a) -> strict multMagma means :Def5: :: TOPALG_1:def 5
( the carrier of it = Class (EqRel (X,a)) & ( for x, y being Element of it ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of it . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) );
existence
ex b1 being strict multMagma st
( the carrier of b1 = Class (EqRel (X,a)) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b1 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) )
proof end;
uniqueness
for b1, b2 being strict multMagma st the carrier of b1 = Class (EqRel (X,a)) & ( for x, y being Element of b1 ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b1 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) & the carrier of b2 = Class (EqRel (X,a)) & ( for x, y being Element of b2 ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b2 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines FundamentalGroup TOPALG_1:def 5 :
for X being non empty TopSpace
for a being Point of X
for b3 being strict multMagma holds
( b3 = FundamentalGroup (X,a) iff ( the carrier of b3 = Class (EqRel (X,a)) & ( for x, y being Element of b3 ex P, Q being Loop of a st
( x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),Q) & the multF of b3 . (x,y) = Class ((EqRel (X,a)),(P + Q)) ) ) ) );

notation
let X be non empty TopSpace;
let a be Point of X;
synonym pi_1 (X,a) for FundamentalGroup (X,a);
end;

registration
let X be non empty TopSpace;
let a be Point of X;
cluster FundamentalGroup (X,a) -> non empty strict ;
coherence
not pi_1 (X,a) is empty
proof end;
end;

theorem Th47: :: TOPALG_1:47
for X being non empty TopSpace
for a being Point of X
for x being set holds
( x in the carrier of (pi_1 (X,a)) iff ex P being Loop of a st x = Class ((EqRel (X,a)),P) )
proof end;

Lm4: for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 (S,s))
for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds
x * y = Class ((EqRel (S,s)),(P + Q))
proof end;

registration
let X be non empty TopSpace;
let a be Point of X;
cluster FundamentalGroup (X,a) -> strict Group-like associative ;
coherence
( pi_1 (X,a) is associative & pi_1 (X,a) is Group-like )
proof end;
end;

definition
let T be non empty TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
assume A1: x0,x1 are_connected ;
func pi_1-iso P -> Function of (pi_1 (T,x1)),(pi_1 (T,x0)) means :Def6: :: TOPALG_1:def 6
 for Q being Loop of x1 holds it . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)));
existence
ex b1 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st
for Q being Loop of x1 holds b1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P)))
proof end;
uniqueness
for b1, b2 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) st ( for Q being Loop of x1 holds b1 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) & ( for Q being Loop of x1 holds b2 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines pi_1-iso TOPALG_1:def 6 :
for T being non empty TopSpace
for x0, x1 being Point of T
for P being Path of x0,x1 st x0,x1 are_connected holds
for b5 being Function of (pi_1 (T,x1)),(pi_1 (T,x0)) holds
( b5 = pi_1-iso P iff for Q being Loop of x1 holds b5 . (Class ((EqRel (T,x1)),Q)) = Class ((EqRel (T,x0)),((P + Q) + (- P))) );

theorem Th48: :: TOPALG_1:48
for X being non empty TopSpace
for x0, x1 being Point of X
for P, Q being Path of x0,x1 st x0,x1 are_connected & P,Q are_homotopic holds
pi_1-iso P = pi_1-iso Q
proof end;

theorem :: TOPALG_1:49
for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R, V being Path of y0,y1 st R,V are_homotopic holds
pi_1-iso R = pi_1-iso V by Th48, BORSUK_2:def 3;

theorem Th50: :: TOPALG_1:50
for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0))
proof end;

registration
let T be non empty pathwise_connected TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
cluster pi_1-iso P -> multiplicative ;
coherence
pi_1-iso P is multiplicative by Th50, BORSUK_2:def 3;
end;

theorem Th51: :: TOPALG_1:51
for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is one-to-one
proof end;

theorem Th52: :: TOPALG_1:52
for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
pi_1-iso P is onto
proof end;

registration
let T be non empty pathwise_connected TopSpace;
let x0, x1 be Point of T;
let P be Path of x0,x1;
cluster pi_1-iso P -> one-to-one onto ;
coherence
( pi_1-iso P is one-to-one & pi_1-iso P is onto ) by Th51, Th52, BORSUK_2:def 3;
end;

theorem Th53: :: TOPALG_1:53
for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
(pi_1-iso P) " = pi_1-iso (- P)
proof end;

theorem :: TOPALG_1:54
for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R being Path of y0,y1 holds (pi_1-iso R) " = pi_1-iso (- R) by Th53, BORSUK_2:def 3;

theorem Th55: :: TOPALG_1:55
for X being non empty TopSpace
for x0, x1 being Point of X
for P being Path of x0,x1 st x0,x1 are_connected holds
for h being Homomorphism of (pi_1 (X,x1)),(pi_1 (X,x0)) st h = pi_1-iso P holds
h is bijective by Th51, Th52;

theorem :: TOPALG_1:56
for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T
for R being Path of y0,y1 holds pi_1-iso R is bijective ;

theorem :: TOPALG_1:57
for X being non empty TopSpace
for x0, x1 being Point of X st x0,x1 are_connected holds
pi_1 (X,x0), pi_1 (X,x1) are_isomorphic
proof end;

theorem :: TOPALG_1:58
for T being non empty pathwise_connected TopSpace
for y0, y1 being Point of T holds pi_1 (T,y0), pi_1 (T,y1) are_isomorphic
proof end;

definition
let n be Nat;
let P, Q be Function of I[01],(TOP-REAL n);
func RealHomotopy (P,Q) -> Function of [:I[01],I[01]:],(TOP-REAL n) means :Def7: :: TOPALG_1:def 7
 for s, t being Element of I[01] holds it . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s));
existence
ex b1 being Function of [:I[01],I[01]:],(TOP-REAL n) st
for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s))
proof end;
uniqueness
for b1, b2 being Function of [:I[01],I[01]:],(TOP-REAL n) st ( for s, t being Element of I[01] holds b1 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) & ( for s, t being Element of I[01] holds b2 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def7 defines RealHomotopy TOPALG_1:def 7 :
for n being Nat
for P, Q being Function of I[01],(TOP-REAL n)
for b4 being Function of [:I[01],I[01]:],(TOP-REAL n) holds
( b4 = RealHomotopy (P,Q) iff for s, t being Element of I[01] holds b4 . (s,t) = ((1 - t) * (P . s)) + (t * (Q . s)) );

Lm5: for n being Nat
for P, Q being continuous Function of I[01],(TOP-REAL n) holds RealHomotopy (P,Q) is continuous
proof end;

Lm6: for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b
for s being Point of I[01] holds
( (RealHomotopy (P,Q)) . (s,0) = P . s & (RealHomotopy (P,Q)) . (s,1) = Q . s & ( for t being Point of I[01] holds
( (RealHomotopy (P,Q)) . (0,t) = a & (RealHomotopy (P,Q)) . (1,t) = b ) ) )
proof end;

theorem Th59: :: TOPALG_1:59
for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds P,Q are_homotopic
proof end;

registration
let n be Nat;
let a, b be Point of (TOP-REAL n);
let P, Q be Path of a,b;
cluster -> continuous for Homotopy of P,Q;
coherence
for b1 being Homotopy of P,Q holds b1 is continuous
proof end;
end;

theorem Th60: :: TOPALG_1:60
for n being Nat
for a being Point of (TOP-REAL n)
for C being Loop of a holds the carrier of (pi_1 ((TOP-REAL n),a)) = {(Class ((EqRel ((TOP-REAL n),a)),C))}
proof end;

registration
let n be Nat;
let a be Point of (TOP-REAL n);
cluster FundamentalGroup ((TOP-REAL n),a) -> trivial strict ;
coherence
pi_1 ((TOP-REAL n),a) is trivial
proof end;
end;

theorem :: TOPALG_1:61
for S being non empty TopSpace
for s being Point of S
for x, y being Element of (pi_1 (S,s))
for P, Q being Loop of s st x = Class ((EqRel (S,s)),P) & y = Class ((EqRel (S,s)),Q) holds
x * y = Class ((EqRel (S,s)),(P + Q)) by Lm4;

:: Added, AK 5.02.2007
theorem Th62: :: TOPALG_1:62
for X being non empty TopSpace
for a being Point of X
for C being constant Loop of a holds 1_ (pi_1 (X,a)) = Class ((EqRel (X,a)),C)
proof end;

theorem :: TOPALG_1:63
for X being non empty TopSpace
for a being Point of X
for x, y being Element of (pi_1 (X,a))
for P being Loop of a st x = Class ((EqRel (X,a)),P) & y = Class ((EqRel (X,a)),(- P)) holds
x " = y
proof end;

registration
let n be Nat;
let P, Q be continuous Function of I[01],(TOP-REAL n);
cluster RealHomotopy (P,Q) -> continuous ;
coherence
RealHomotopy (P,Q) is continuous by Lm5;
end;

theorem :: TOPALG_1:64
for n being Nat
for a, b being Point of (TOP-REAL n)
for P, Q being Path of a,b holds RealHomotopy (P,Q) is Homotopy of P,Q
proof end;

theorem :: TOPALG_1:65
for X being non empty TopSpace
for a, b being Point of X st a,b are_connected holds
( not EqRel (X,a,b) is empty & EqRel (X,a,b) is total & EqRel (X,a,b) is symmetric & EqRel (X,a,b) is transitive ) by Lm3;