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


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 ;
proof end;
end;

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

theorem Th2: :: TOPALG_6:2
for r1, r2, r3, r4, r5, r6 being Real st r1 < r2 & r3 <= r4 & r5 < r6 holds
(L[01] (r1,r2,r3,r4)) * (L[01] (r5,r6,r1,r2)) = L[01] (r5,r6,r3,r4)
proof end;

registration
let n be positive Nat;
cluster TOP-REAL n -> infinite ;
correctness
coherence
not TOP-REAL n is finite ;
proof end;
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 ;
proof end;
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}
proof end;

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 & sup (dom p) = 1 )
proof end;

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
proof end;

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 & t1,t2 are_connected & A = C & B = D & C,D are_homotopic holds
A,B are_homotopic
proof end;

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 & t1,t2 are_connected & A = C & B = D & 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)
proof end;

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))}
proof end;

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 & S = ([#] (TOP-REAL n)) \ {p} holds
(TOP-REAL n) | S is pathwise_connected
proof end;

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 & S = ([#] T) \ {t} & TOP-REAL n,T are_homeomorphic holds
T | S is pathwise_connected
proof end;

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 ;
proof end;
end;

definition
let T be non empty TopSpace;
attr T 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;
attr T is simply_connected means :: TOPALG_6:def 2
( T is having_trivial_Fundamental_Group & T is pathwise_connected );
end;

:: deftheorem 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 & 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 & b1 is pathwise_connected ) ;
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 & b1 is pathwise_connected holds
b1 is simply_connected ;
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
proof end;

registration
let n be Nat;
cluster TOP-REAL n -> having_trivial_Fundamental_Group ;
coherence
TOP-REAL n is having_trivial_Fundamental_Group ;
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
proof end;
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 & ( for P, Q being Path of t1,t2 holds Class ((EqRel (T,t1,t2)),P) = Class ((EqRel (T,t1,t2)),Q) ) ) )
proof end;

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 & S is having_trivial_Fundamental_Group holds
T is having_trivial_Fundamental_Group
proof end;

theorem Th14: :: TOPALG_6:14
for S, T being non empty TopSpace st S,T are_homeomorphic & S is simply_connected holds
T is simply_connected by Th13, TOPALG_3:9;

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
proof end;

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

:: deftheorem 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 by BORSUK_6:88;
end;

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

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;
cluster f * 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
proof end;
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
proof end;

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 ;
;
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 & f = g & g is nullhomotopic holds
f is nullhomotopic
proof end;

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

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

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 ;
proof end;
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)))
proof end;
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
proof end;
end;

definition
let T be TopStruct ;
mode Curve of T is Element of Curves T;
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
proof end;

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

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
proof end;

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
proof end;

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

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

definition
let T be TopStruct ;
let c be Curve of T;
attr c is with_first_point means :Def6: :: TOPALG_6:def 6
 dom c is left_end ;
attr c 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;
attr c is with_endpoints means :: TOPALG_6:def 8
( c is with_first_point & c is with_last_point );
end;

:: deftheorem 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 & 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 & b1 is with_last_point holds
b1 is with_endpoints ;
;
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 & b1 is with_last_point );
;
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 ;
proof end;
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 ;
proof end;
cluster inf (dom c) -> real ;
correctness
coherence
inf (dom c) is real ;
proof end;
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 ;
proof end;
cluster sup (dom c) -> real ;
correctness
coherence
sup (dom c) is real ;
proof end;
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 ;
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 ;
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;
proof end;
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;
proof end;
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
proof end;

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

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)).]
proof end;

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
proof end;

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
proof end;

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 & t1,t2 are_connected holds
( t1 = the_first_point_of c & t2 = the_last_point_of c )
proof end;

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 & the_last_point_of c in rng c )
proof end;

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

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
proof end;

definition
let T be non empty TopStruct ;
let c1, c2 be with_endpoints Curve of T;
pred c1,c2 are_homotopic means :: 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)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & 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)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & 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)))) & p2 = c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) & p1,p2 are_homotopic ) ;
end;

:: deftheorem 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)))) & p2 = c2 * (L[01] (0,1,(inf (dom c2)),(sup (dom c2)))) & p1,p2 are_homotopic ) );

definition
let T be non empty TopSpace;
let c1, c2 be with_endpoints Curve of T;
:: original: are_homotopic
redefine pred c1,c2 are_homotopic ;
reflexivity
for c1 being with_endpoints Curve of T holds (T,b1,b1)
proof end;
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 & c2 = p2 & a,b are_connected holds
( c1,c2 are_homotopic iff p1,p2 are_homotopic )
proof end;

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 & the_last_point_of c1 = the_last_point_of c2 )
proof end;

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 & 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 & ( for t being Point of (R^1 | S) holds
( f . (t,0) = c1 . t & f . (t,1) = c2 . t ) ) & ( for t being Point of I[01] holds
( f . ((inf S),t) = a & f . ((sup S),t) = b ) ) ) )
proof end;

definition
let T be TopStruct ;
let c1, c2 be Curve of T;
func c1 + 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 ) & ( c1 \/ c2 is not Curve of T implies {} is Curve of T ) );
consistency
for b1 being Curve of T holds verum;
proof end;
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 ) & ( 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 ex c1, c2 being Element of Curves T st
( c = c1 + c2 & c1 = c | [.(inf (dom c)),r.] & c2 = c | [.r,(sup (dom c)).] )
proof end;

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) & the_last_point_of c1 = the_first_point_of c2 holds
( c1 + c2 is with_endpoints & dom (c1 + c2) = [.(inf (dom c1)),(sup (dom c2)).] & (c1 + c2) . (inf (dom c1)) = the_first_point_of c1 & (c1 + c2) . (sup (dom c2)) = the_last_point_of c2 )
proof end;

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 & dom c1 = dom c2 & c3,c4 are_homotopic & dom c3 = dom c4 & c5 = c1 + c3 & c6 = c2 + c4 & the_last_point_of c1 = the_first_point_of c3 & sup (dom c1) = inf (dom c3) holds
c5,c6 are_homotopic
proof end;

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 & f . 1 = it . 1 & ( for i being Nat st 1 <= i & 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 & f . 1 = b1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of Curves T st len f = len b1 & f . 1 = b1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b1 . (i + 1) = (b1 /. i) + (f /. (i + 1)) ) & len f = len b2 & f . 1 = b2 . 1 & ( for i being Nat st 1 <= i & i < len f holds
b2 . (i + 1) = (b2 /. i) + (f /. (i + 1)) ) holds
b1 = b2
proof end;
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 & f . 1 = b3 . 1 & ( for i being Nat st 1 <= i & 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 ) & ( not len f > 0 implies {} is Curve of T ) )
proof end;
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) ) & ( 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
proof end;

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)
proof end;

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
proof end;

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 & i <= len f holds
rng (f /. i) c= X ) holds
rng (Sum f) c= X
proof end;

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

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 & len f1 = len f2 & Sum f1 = c1 & Sum f2 = c2 & ( for i being Nat st 1 <= i & i < len f1 holds
( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i < len f2 holds
( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) & ( for i being Nat st 1 <= i & i <= len f1 holds
ex c3, c4 being with_endpoints Curve of T st
( c3 = f1 /. i & c4 = f2 /. i & c3,c4 are_homotopic & dom c3 = dom c4 ) ) holds
c1,c2 are_homotopic
proof end;

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 & h . 1 = inf (dom c) & h . (len h) = sup (dom c) & h is increasing holds
ex f being FinSequence of Curves T st
( len f = (len h) - 1 & c = Sum f & ( for i being Nat st 1 <= i & i <= len f holds
f /. i = c | [.(h /. i),(h /. (i + 1)).] ) )
proof end;

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
proof end;

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

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

theorem :: TOPALG_6:47
for n being non zero Nat
for r being positive Real
for x being Point of (TOP-REAL n) st n >= 3 holds
Tcircle (x,r) is having_trivial_Fundamental_Group
proof end;