:: Fundamental Group of $n$-sphere for $n \geq 2$
:: by Marco Riccardi and Artur Korni{\l}owicz
::
:: Received November 3, 2011
:: Copyright (c) 2011-2012 Association of Mizar Users


begin

registration
let S be TopSpace;
let T be non empty TopSpace;
cluster Function-like constant quasi_total  ->  continuous for Element of bool [: the carrier of S, the carrier of T:];
correctness
coherence
for b1 being Function of S,T st b1 is constant holds
b1 is continuous ;
proofend;
end;

theorem Th1: :: TOPALG_6:1
L[01] (0,1,0,1) = id (Closed-Interval-TSpace (0,1))
proofend;

theorem Th2: :: TOPALG_6:2
for r1, r2, r3, r4, r5, r6 being real number st r1 < r2 &amp; r3 <= r4 &amp; r5 < r6 holds
(L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4)
proofend;

registration
let n be positive Nat;
cluster TOP-REAL n ->  infinite ;
correctness
coherence
not TOP-REAL n is finite ;
proofend;
cluster non empty TopSpace-like n -locally_euclidean  ->  non empty infinite for TopStruct ;
correctness
coherence
for b1 being non empty TopSpace st b1 is n -locally_euclidean holds
b1 is infinite ;
proofend;
end;

theorem Th3: :: TOPALG_6:3
for n being Nat
for p being Point of (TOP-REAL n) st p in Sphere ((0. (TOP-REAL n)),1) holds
- p in (Sphere ((0. (TOP-REAL n)),1)) \ {p}
proofend;

theorem Th4: :: TOPALG_6:4
for T being non empty TopStruct
for t1, t2 being Point of T
for p being Path of t1,t2 holds
( inf (dom p) = 0 &amp; sup (dom p) = 1 )
proofend;

theorem Th5: :: TOPALG_6:5
for T being non empty TopSpace
for t being Point of T
for C1, C2 being constant Loop of t holds C1,C2 are_homotopic
proofend;

theorem Th6: :: TOPALG_6:6
for T being non empty TopSpace
for S being non empty SubSpace of T
for t1, t2 being Point of T
for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected &amp; t1,t2 are_connected &amp; A = C &amp; B = D &amp; C,D are_homotopic holds
A,B are_homotopic
proofend;

theorem :: TOPALG_6:7
for T being non empty TopSpace
for S being non empty SubSpace of T
for t1, t2 being Point of T
for s1, s2 being Point of S
for A, B being Path of t1,t2
for C, D being Path of s1,s2 st s1,s2 are_connected &amp; t1,t2 are_connected &amp; A = C &amp; B = D &amp; Class ((EqRel (S,s1,s2)),C) = Class ((EqRel (S,s1,s2)),D) holds
Class ((EqRel (T,t1,t2)),A) = Class ((EqRel (T,t1,t2)),B)
proofend;

theorem Th8: :: TOPALG_6:8
for T being non empty trivial TopSpace
for t being Point of T
for L being Loop of t holds the carrier of (pi_1 (T,t)) = {(Class ((EqRel (T,t)),L))}
proofend;

theorem Th9: :: TOPALG_6:9
for n being Nat
for p being Point of (TOP-REAL n)
for S being Subset of (TOP-REAL n) st n >= 2 &amp; S = ([#] (TOP-REAL n)) \ {p} holds
(TOP-REAL n) | S is pathwise_connected
proofend;

theorem Th10: :: TOPALG_6:10
for T being non empty TopSpace
for t being Point of T
for n being Nat
for S being non empty Subset of T st n >= 2 &amp; S = ([#] T) \ {t} &amp; TOP-REAL n,T are_homeomorphic holds
T | S is pathwise_connected
proofend;

registration
let n be Element of NAT ;
let p, q be Point of (TOP-REAL n);
cluster TPlane (p,q) ->  convex ;
correctness
coherence
TPlane (p,q) is convex ;
proofend;
end;

begin

definition
let T be non empty TopSpace;
attrT is having_trivial_Fundamental_Group  means :Def1: :: TOPALG_6:def 1
 for t being Point of T holds pi_1 (T,t) is trivial ;
end;

:: deftheorem Def1 defines having_trivial_Fundamental_Group TOPALG_6:def_1_:_
 for T being non empty TopSpace holds
( T is having_trivial_Fundamental_Group iff for t being Point of T holds pi_1 (T,t) is trivial );

definition
let T be non empty TopSpace;
attrT is simply_connected  means :Def2: :: TOPALG_6:def 2
( T is having_trivial_Fundamental_Group &amp; T is pathwise_connected );
end;

:: deftheorem Def2 defines simply_connected TOPALG_6:def_2_:_
 for T being non empty TopSpace holds
( T is simply_connected iff ( T is having_trivial_Fundamental_Group &amp; T is pathwise_connected ) );

registration
cluster non empty TopSpace-like simply_connected  ->  non empty pathwise_connected having_trivial_Fundamental_Group for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is simply_connected holds
( b1 is having_trivial_Fundamental_Group &amp; b1 is pathwise_connected ) by Def2;
cluster non empty TopSpace-like pathwise_connected having_trivial_Fundamental_Group  ->  non empty simply_connected for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is having_trivial_Fundamental_Group &amp; b1 is pathwise_connected holds
b1 is simply_connected by Def2;
end;

theorem Th11: :: TOPALG_6:11
for T being non empty TopSpace st T is having_trivial_Fundamental_Group holds
for t being Point of T
for P, Q being Loop of t holds P,Q are_homotopic
proofend;

registration
let n be Nat;
cluster TOP-REAL n ->  having_trivial_Fundamental_Group ;
coherence
 TOP-REAL n is having_trivial_Fundamental_Group
proofend;
end;

registration
cluster non empty trivial TopSpace-like  ->  non empty having_trivial_Fundamental_Group for TopStruct ;
coherence
 for b1 being non empty TopSpace st b1 is trivial holds
b1 is having_trivial_Fundamental_Group
proofend;
end;

theorem Th12: :: TOPALG_6:12
for T being non empty TopSpace holds
( T is simply_connected iff for t1, t2 being Point of T holds
( t1,t2 are_connected &amp; ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) )
proofend;

registration
let T be non empty having_trivial_Fundamental_Group TopSpace;
let t be Point of T;
cluster FundamentalGroup (T,t) ->  trivial ;
coherence
 pi_1 (T,t) is trivial by Def1;
end;

theorem Th13: :: TOPALG_6:13
for S, T being non empty TopSpace st S,T are_homeomorphic &amp; S is having_trivial_Fundamental_Group holds
T is having_trivial_Fundamental_Group
proofend;

theorem Th14: :: TOPALG_6:14
for S, T being non empty TopSpace st S,T are_homeomorphic &amp; S is simply_connected holds
T is simply_connected
proofend;

theorem Th15: :: TOPALG_6:15
for T being non empty having_trivial_Fundamental_Group TopSpace
for t being Point of T
for P1, P2 being Loop of t holds P1,P2 are_homotopic
proofend;

definition
let T be non empty TopSpace;
let t be Point of T;
let l be Loop of t;
attrl is nullhomotopic  means :Def3: :: TOPALG_6:def 3
 ex c being constant Loop of t st l,c are_homotopic ;
end;

:: deftheorem Def3 defines nullhomotopic TOPALG_6:def_3_:_
 for T being non empty TopSpace
for t being Point of T
for l being Loop of t holds
( l is nullhomotopic iff ex c being constant Loop of t st l,c are_homotopic );

registration
let T be non empty TopSpace;
let t be Point of T;
cluster constant  ->  nullhomotopic for Path of t,t;
coherence
 for b1 being Loop of t st b1 is constant holds
b1 is nullhomotopic
proofend;
end;

registration
let T be non empty TopSpace;
let t be Point of T;
cluster non empty Relation-like the carrier of I[01] -defined the carrier of T -valued Function-like constant total quasi_total continuous for Path of t,t;
existence
 ex b1 being Loop of t st b1 is constant
proofend;
end;

theorem Th16: :: TOPALG_6:16
for T, U being non empty TopSpace
for t being Point of T
for f being Loop of t
for g being continuous Function of T,U st f is nullhomotopic holds
g * f is nullhomotopic
proofend;

registration
let T, U be non empty TopSpace;
let t be Point of T;
let f be nullhomotopic Loop of t;
let g be continuous Function of T,U;
clusterf * g ->  nullhomotopic for Loop of g . t;
coherence
 for b1 being Loop of g . t st b1 = g * f holds
b1 is nullhomotopic by Th16;
end;

registration
let T be non empty having_trivial_Fundamental_Group TopSpace;
let t be Point of T;
cluster  ->  nullhomotopic for Path of t,t;
coherence
 for b1 being Loop of t holds b1 is nullhomotopic
proofend;
end;

theorem Th17: :: TOPALG_6:17
for T being non empty TopSpace st ( for t being Point of T
for f being Loop of t holds f is nullhomotopic ) holds
T is having_trivial_Fundamental_Group
proofend;

registration
let n be Element of NAT ;
let p, q be Point of (TOP-REAL n);
cluster TPlane (p,q) ->  having_trivial_Fundamental_Group ;
correctness
coherence
TPlane (p,q) is having_trivial_Fundamental_Group ;
proofend;
end;

theorem Th18: :: TOPALG_6:18
for T being non empty TopSpace
for t being Point of T
for S being non empty SubSpace of T
for s being Point of S
for f being Loop of t
for g being Loop of s st t = s &amp; f = g &amp; g is nullhomotopic holds
f is nullhomotopic
proofend;

begin

definition
let T be TopStruct ;
let f be PartFunc of R^1,T;
attrf is parametrized-curve  means :Def4: :: TOPALG_6:def 4
( dom f is interval Subset of REAL &amp; ex S being SubSpace of R^1 ex g being Function of S,T st
( f = g &amp; S = R^1 | (dom f) &amp; g is continuous ) );
end;

:: deftheorem Def4 defines parametrized-curve TOPALG_6:def_4_:_
 for T being TopStruct
for f being PartFunc of R^1,T holds
( f is parametrized-curve iff ( dom f is interval Subset of REAL &amp; ex S being SubSpace of R^1 ex g being Function of S,T st
( f = g &amp; S = R^1 | (dom f) &amp; g is continuous ) ) );

Lm1:  for T being TopStruct
for f being PartFunc of R^1,T st f = {} holds
f is parametrized-curve
proofend;

registration
let T be TopStruct ;
cluster Relation-like the carrier of R^1 -defined the carrier of T -valued Function-like parametrized-curve for Element of bool [: the carrier of R^1, the carrier of T:];
correctness
existence
ex b1 being PartFunc of R^1,T st b1 is parametrized-curve ;
proofend;
end;

theorem :: TOPALG_6:19
for T being TopStruct holds {} is parametrized-curve PartFunc of R^1,T by Lm1, XBOOLE_1:2;

definition
let T be TopStruct ;
func Curves T ->  Subset of (PFuncs (REAL,([#] T))) equals :: TOPALG_6:def 5
 {  f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T  }  ;
coherence
  {  f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T  }  is Subset of (PFuncs (REAL,([#] T)))
proofend;
end;

:: deftheorem  defines Curves TOPALG_6:def_5_:_
 for T being TopStruct holds Curves T =  {  f where f is Element of PFuncs (REAL,([#] T)) : f is parametrized-curve PartFunc of R^1,T  }  ;

registration
let T be TopStruct ;
cluster Curves T ->  non empty ;
coherence
 not Curves T is empty
proofend;
end;

definition
let T be TopStruct ;
mode Curve of T is Element of Curves T;
correctness
;
end;

theorem Th20: :: TOPALG_6:20
for T being TopStruct
for f being parametrized-curve PartFunc of R^1,T holds f is Curve of T
proofend;

theorem Th21: :: TOPALG_6:21
for T being TopStruct holds {} is Curve of T
proofend;

theorem Th22: :: TOPALG_6:22
for T being TopStruct
for t1, t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected holds
p is Curve of T
proofend;

theorem Th23: :: TOPALG_6:23
for T being TopStruct
for c being Curve of T holds c is parametrized-curve PartFunc of R^1,T
proofend;

theorem Th24: :: TOPALG_6:24
for T being TopStruct
for c being Curve of T holds
( dom c c= REAL &amp; rng c c= [#] T )
proofend;

registration
let T be TopStruct ;
let c be Curve of T;
cluster dom c ->  real-membered ;
correctness
coherence
dom c is real-membered ;
proofend;
end;

definition
let T be TopStruct ;
let c be Curve of T;
attrc is with_first_point  means :Def6: :: TOPALG_6:def 6
 dom c is left_end ;
attrc is with_last_point  means :Def7: :: TOPALG_6:def 7
 dom c is right_end ;
end;

:: deftheorem Def6 defines with_first_point TOPALG_6:def_6_:_
 for T being TopStruct
for c being Curve of T holds
( c is with_first_point iff dom c is left_end );

:: deftheorem Def7 defines with_last_point TOPALG_6:def_7_:_
 for T being TopStruct
for c being Curve of T holds
( c is with_last_point iff dom c is right_end );

definition
let T be TopStruct ;
let c be Curve of T;
attrc is with_endpoints  means :Def8: :: TOPALG_6:def 8
( c is with_first_point &amp; c is with_last_point );
end;

:: deftheorem Def8 defines with_endpoints TOPALG_6:def_8_:_
 for T being TopStruct
for c being Curve of T holds
( c is with_endpoints iff ( c is with_first_point &amp; c is with_last_point ) );

registration
let T be TopStruct ;
cluster with_first_point with_last_point  ->  with_endpoints for Element of Curves T;
correctness
coherence
for b1 being Curve of T st b1 is with_first_point &amp; b1 is with_last_point holds
b1 is with_endpoints ;
by Def8;
cluster with_endpoints  ->  with_first_point with_last_point for Element of Curves T;
correctness
coherence
for b1 being Curve of T st b1 is with_endpoints holds
( b1 is with_first_point &amp; b1 is with_last_point );
by Def8;
end;

registration
let T be non empty TopStruct ;
cluster Relation-like Function-like with_endpoints for Element of Curves T;
correctness
existence
ex b1 being Curve of T st b1 is with_endpoints ;
proofend;
end;

registration
let T be non empty TopStruct ;
let c be with_first_point Curve of T;
cluster dom c ->  non empty ;
correctness
coherence
not dom c is empty ;
proofend;
cluster inf (dom c) ->  real ;
correctness
coherence
inf (dom c) is real ;
proofend;
end;

registration
let T be non empty TopStruct ;
let c be with_last_point Curve of T;
cluster dom c ->  non empty ;
correctness
coherence
not dom c is empty ;
proofend;
cluster sup (dom c) ->  real ;
correctness
coherence
sup (dom c) is real ;
proofend;
end;

registration
let T be non empty TopStruct ;
cluster with_first_point  ->  non empty for Element of Curves T;
coherence
 for b1 being Curve of T st b1 is with_first_point holds
not b1 is empty
proofend;
cluster with_last_point  ->  non empty for Element of Curves T;
coherence
 for b1 being Curve of T st b1 is with_last_point holds
not b1 is empty
proofend;
end;

definition
let T be non empty TopStruct ;
let c be with_first_point Curve of T;
func the_first_point_of c ->  Point of T equals :: TOPALG_6:def 9
c . (inf (dom c));
correctness
coherence
c . (inf (dom c)) is Point of T;
proofend;
end;

:: deftheorem  defines the_first_point_of TOPALG_6:def_9_:_
 for T being non empty TopStruct
for c being with_first_point Curve of T holds the_first_point_of c = c . (inf (dom c));

definition
let T be non empty TopStruct ;
let c be with_last_point Curve of T;
func the_last_point_of c ->  Point of T equals :: TOPALG_6:def 10
c . (sup (dom c));
correctness
coherence
c . (sup (dom c)) is Point of T;
proofend;
end;

:: deftheorem  defines the_last_point_of TOPALG_6:def_10_:_
 for T being non empty TopStruct
for c being with_last_point Curve of T holds the_last_point_of c = c . (sup (dom c));

theorem Th25: :: TOPALG_6:25
for T being non empty TopStruct
for t1, t2 being Point of T
for p being Path of t1,t2 st t1,t2 are_connected holds
p is with_endpoints Curve of T
proofend;

theorem Th26: :: TOPALG_6:26
for T being non empty TopStruct
for c being Curve of T
for r1, r2 being real number holds c | [.r1,r2.] is Curve of T
proofend;

theorem Th27: :: TOPALG_6:27
for T being non empty TopStruct
for c being with_endpoints Curve of T holds dom c = [.(inf (dom c)),(sup (dom c)).]
proofend;

theorem Th28: :: TOPALG_6:28
for T being non empty TopStruct
for c being with_endpoints Curve of T st dom c = [.0,1.] holds
c is Path of the_first_point_of c, the_last_point_of c
proofend;

theorem Th29: :: TOPALG_6:29
for T being non empty TopStruct
for c being with_endpoints Curve of T holds c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of the_first_point_of c, the_last_point_of c
proofend;

theorem :: TOPALG_6:30
for T being non empty TopStruct
for c being with_endpoints Curve of T
for t1, t2 being Point of T st c * (L[01] (0,1,(inf (dom c)),(sup (dom c)))) is Path of t1,t2 &amp; t1,t2 are_connected holds
( t1 = the_first_point_of c &amp; t2 = the_last_point_of c )
proofend;

theorem Th31: :: TOPALG_6:31
for T being non empty TopStruct
for c being with_endpoints Curve of T holds
( the_first_point_of c in rng c &amp; the_last_point_of c in rng c )
proofend;

theorem Th32: :: TOPALG_6:32
for T being non empty TopStruct
for r1, r2 being real number
for t1, t2 being Point of T
for p1 being Path of t1,t2 st t1,t2 are_connected &amp; r1 < r2 holds
p1 * (L[01] (r1,r2,0,1)) is with_endpoints Curve of T
proofend;

theorem Th33: :: TOPALG_6:33
for T being non empty TopStruct
for c being with_endpoints Curve of T holds the_first_point_of c, the_last_point_of c are_connected
proofend;

definition
let T be non empty TopStruct ;
let c1, c2 be with_endpoints Curve of T;
predc1,c2 are_homotopic  means :Def11: :: TOPALG_6:def 11
 ex a, b being Point of T ex p1, p2 being Path of a,b st
( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &amp; p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &amp; p1,p2 are_homotopic );
symmetry
 for c1, c2 being with_endpoints Curve of T st ex a, b being Point of T ex p1, p2 being Path of a,b st
( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &amp; p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &amp; p1,p2 are_homotopic ) holds
ex a, b being Point of T ex p1, p2 being Path of a,b st
( p1 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &amp; p2 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &amp; p1,p2 are_homotopic ) ;
end;

:: deftheorem Def11 defines are_homotopic TOPALG_6:def_11_:_
 for T being non empty TopStruct
for c1, c2 being with_endpoints Curve of T holds
( c1,c2 are_homotopic iff ex a, b being Point of T ex p1, p2 being Path of a,b st
( p1 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) &amp; p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) &amp; p1,p2 are_homotopic ) );

definition
let T be non empty TopSpace;
let c1, c2 be with_endpoints Curve of T;
:: original:are_homotopic
redefine predc1,c2 are_homotopic ;
reflexivity
 for c1 being with_endpoints Curve of T holds (T,b1,b1)
proofend;
symmetry
 for c1, c2 being with_endpoints Curve of T st (T,b1,b2) holds
(T,b2,b1) ;
end;

theorem Th34: :: TOPALG_6:34
for T being non empty TopStruct
for c1, c2 being with_endpoints Curve of T
for a, b being Point of T
for p1, p2 being Path of a,b st c1 = p1 &amp; c2 = p2 &amp; a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )
proofend;

theorem Th35: :: TOPALG_6:35
for T being non empty TopStruct
for c1, c2 being with_endpoints Curve of T st c1,c2 are_homotopic holds
( the_first_point_of c1 = the_first_point_of c2 &amp; the_last_point_of c1 = the_last_point_of c2 )
proofend;

theorem Th36: :: TOPALG_6:36
for T being non empty TopSpace
for c1, c2 being with_endpoints Curve of T
for S being Subset of R^1 st dom c1 = dom c2 &amp; S = dom c1 holds
( c1,c2 are_homotopic iff ex f being Function of [:(R^1 | S),I[01]:],T ex a, b being Point of T st
( f is continuous &amp; ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t &amp; f . (t,1) = c2 . t ) ) &amp; ( for t being Point of I[01] holds
( f . ((inf S),t) = a &amp; f . ((sup S),t) = b ) ) ) )
proofend;

definition
let T be TopStruct ;
let c1, c2 be Curve of T;
funcc1 + c2 ->  Curve of T equals :Def12: :: TOPALG_6:def 12
c1 \/ c2 if c1 \/ c2 is Curve of T
otherwise  {} ;
correctness
coherence
( ( c1 \/ c2 is Curve of T implies c1 \/ c2 is Curve of T ) &amp; ( c1 \/ c2 is not Curve of T implies {} is Curve of T ) );
consistency
for b1 being Curve of T holds verum;
proofend;
end;

:: deftheorem Def12 defines + TOPALG_6:def_12_:_
 for T being TopStruct
for c1, c2 being Curve of T holds
( ( c1 \/ c2 is Curve of T implies c1 + c2 = c1 \/ c2 ) &amp; ( c1 \/ c2 is not Curve of T implies c1 + c2 = {} ) );

theorem Th37: :: TOPALG_6:37
for T being non empty TopStruct
for c being with_endpoints Curve of T
for r being real number ex c1, c2 being Element of Curves T st
( c = c1 + c2 &amp; c1 = c | [.(inf (dom c)),r.] &amp; c2 = c | [.r,(sup (dom c)).] )
proofend;

theorem Th38: :: TOPALG_6:38
for T being non empty TopSpace
for c1, c2 being with_endpoints Curve of T st sup (dom c1) = inf (dom c2) &amp; the_last_point_of c1 = the_first_point_of c2 holds
( c1 + c2 is with_endpoints &amp; dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] &amp; (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 &amp; (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
proofend;

theorem Th39: :: TOPALG_6:39
for T being non empty TopSpace
for c1, c2, c3, c4, c5, c6 being with_endpoints Curve of T st c1,c2 are_homotopic &amp; dom c1 = dom c2 &amp; c3,c4 are_homotopic &amp; dom c3 = dom c4 &amp; c5 = c1 + c3 &amp; c6 = c2 + c4 &amp; the_last_point_of c1 = the_first_point_of c3 &amp; sup (dom c1) = inf (dom c3) holds
c5,c6 are_homotopic
proofend;

definition
let T be TopStruct ;
let f be FinSequence of Curves T;
func Partial_Sums f ->  FinSequence of Curves T means :Def13: :: TOPALG_6:def 13
( len f = len it &amp; f . 1 = it . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
it . (i + 1) = (it /. i) + (f /. (i + 1)) ) );
existence
 ex b1 being FinSequence of Curves T st
( len f = len b1 &amp; f . 1 = b1 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of Curves T st len f = len b1 &amp; f . 1 = b1 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) &amp; len f = len b2 &amp; f . 1 = b2 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b2 . (i + 1) = (b2 /. i) + (f /. (i + 1)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines Partial_Sums TOPALG_6:def_13_:_
 for T being TopStruct
for f, b3 being FinSequence of Curves T holds
( b3 = Partial_Sums f iff ( len f = len b3 &amp; f . 1 = b3 . 1 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
b3 . (i + 1) = (b3 /. i) + (f /. (i + 1)) ) ) );

definition
let T be TopStruct ;
let f be FinSequence of Curves T;
func Sum f ->  Curve of T equals :Def14: :: TOPALG_6:def 14
(Partial_Sums f) . (len f) if  len f > 0
otherwise  {} ;
coherence
 ( ( len f > 0 implies (Partial_Sums f) . (len f) is Curve of T ) &amp; ( not len f > 0 implies {} is Curve of T ) )
proofend;
consistency
 for b1 being Curve of T holds verum ;
end;

:: deftheorem Def14 defines Sum TOPALG_6:def_14_:_
 for T being TopStruct
for f being FinSequence of Curves T holds
( ( len f > 0 implies Sum f = (Partial_Sums f) . (len f) ) &amp; ( not len f > 0 implies Sum f = {} ) );

theorem Th40: :: TOPALG_6:40
for T being non empty TopStruct
for c being Curve of T holds Sum <*c*> = c
proofend;

Lm2:  for T being non empty TopStruct
for f1, f2 being FinSequence of Curves T holds (Partial_Sums (f1 ^ f2)) . (len f1) = (Partial_Sums f1) . (len f1)
proofend;

theorem Th41: :: TOPALG_6:41
for T being non empty TopStruct
for c being Curve of T
for f being FinSequence of Curves T holds Sum (f ^ <*c*>) = (Sum f) + c
proofend;

theorem Th42: :: TOPALG_6:42
for T being non empty TopStruct
for X being set
for f being FinSequence of Curves T st ( for i being Nat st 1 <= i &amp; i <= len f holds
rng (f /. i) c= X ) holds
rng (Sum f) c= X
proofend;

theorem Th43: :: TOPALG_6:43
for T being non empty TopSpace
for f being FinSequence of Curves T st len f > 0 &amp; ( for i being Nat st 1 <= i &amp; i < len f holds
( (f /. i) . (sup (dom (f /. i))) = (f /. (i + 1)) . (inf (dom (f /. (i + 1)))) &amp; sup (dom (f /. i)) = inf (dom (f /. (i + 1))) ) ) &amp; ( for i being Nat st 1 <= i &amp; i <= len f holds
f /. i is with_endpoints ) holds
ex c being with_endpoints Curve of T st
( Sum f = c &amp; dom c = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] &amp; the_first_point_of c = (f /. 1) . (inf (dom (f /. 1))) &amp; the_last_point_of c = (f /. (len f)) . (sup (dom (f /. (len f)))) )
proofend;

theorem Th44: :: TOPALG_6:44
for T being non empty TopSpace
for f1, f2 being FinSequence of Curves T
for c1, c2 being with_endpoints Curve of T st len f1 > 0 &amp; len f1 = len f2 &amp; Sum f1 = c1 &amp; Sum f2 = c2 &amp; ( for i being Nat st 1 <= i &amp; i < len f1 holds
( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) &amp; sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) &amp; ( for i being Nat st 1 <= i &amp; i < len f2 holds
( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) &amp; sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) &amp; ( for i being Nat st 1 <= i &amp; i <= len f1 holds
ex c3, c4 being with_endpoints Curve of T st
( c3 = f1 /. i &amp; c4 = f2 /. i &amp; c3,c4 are_homotopic &amp; dom c3 = dom c4 ) ) holds
c1,c2 are_homotopic
proofend;

theorem Th45: :: TOPALG_6:45
for T being non empty TopStruct
for c being with_endpoints Curve of T
for h being FinSequence of REAL st len h >= 2 &amp; h . 1 = inf (dom c) &amp; h . (len h) = sup (dom c) &amp; h is increasing holds
ex f being FinSequence of Curves T st
( len f = (len h) - 1 &amp; c = Sum f &amp; ( for i being Nat st 1 <= i &amp; i <= len f holds
f /. i = c | [.(h /. i),(h /. (i + 1)).] ) )
proofend;

Lm3:  for n being Nat
for t being Point of (TUnitSphere n)
for f being Loop of t st rng f <> the carrier of (TUnitSphere n) holds
f is nullhomotopic
proofend;

Lm4:  for n being Nat
for t being Point of (TUnitSphere n)
for f being Loop of t st n >= 2 &amp; rng f = the carrier of (TUnitSphere n) holds
ex g being Loop of t st
( g,f are_homotopic &amp; rng g <> the carrier of (TUnitSphere n) )
proofend;

theorem Th46: :: TOPALG_6:46
for n being Nat st n >= 2 holds
TUnitSphere n is having_trivial_Fundamental_Group
proofend;

theorem :: TOPALG_6:47
for n being non empty Nat
for r being real positive number
for x being Point of (TOP-REAL n) st n >= 3 holds
Tcircle (x,r) is having_trivial_Fundamental_Group
proofend;