:: 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 b₁ being Function of S,T st b₁ is constant holds
b₁ 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 b₁ being non empty TopSpace st b₁ is n -locally_euclidean holds
b₁ 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 b₁ being non empty TopSpace st b₁ is simply_connected holds
( b₁ is having_trivial_Fundamental_Group & b₁ is pathwise_connected ) ;

cluster non empty TopSpace-like pathwise_connected having_trivial_Fundamental_Group -> non empty simply_connected for TopStruct ;

coherence
for b₁ being non empty TopSpace st b₁ is having_trivial_Fundamental_Group & b₁ is pathwise_connected holds
b₁ 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 b₁ being non empty TopSpace st b₁ is trivial holds
b₁ 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 b₁ being Loop of t st b₁ is constant holds
b₁ 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 b₁ being Loop of t st b₁ 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 b₁ being Loop of g . t st b₁ = g * f holds
b₁ 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 b₁ being Loop of t holds b₁ 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 b₁ being PartFunc of R^1,T st b₁ 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 b₁ being Curve of T st b₁ is with_first_point & b₁ is with_last_point holds
b₁ is with_endpoints ;
;

cluster with_endpoints -> with_first_point with_last_point for Element of Curves T;

correctness
coherence
for b₁ being Curve of T st b₁ is with_endpoints holds
( b₁ is with_first_point & b₁ 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 b₁ being Curve of T st b₁ 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 b₁ being Curve of T st b₁ is with_first_point holds
not b₁ is empty ;

cluster with_last_point -> non empty for Element of Curves T;

coherence
for b₁ being Curve of T st b₁ is with_last_point holds
not b₁ 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,b₁,b₁)

proof end;

symmetry
for c1, c2 being with_endpoints Curve of T st (T,b₁,b₂) holds
(T,b₂,b₁) ;

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 b₁ 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 b₁ being FinSequence of Curves T st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of Curves T st len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) & len f = len b₂ & f . 1 = b₂ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₂ . (i + 1) = (b₂ /. i) + (f /. (i + 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines Partial_Sums TOPALG_6:def 13 :
for T being TopStruct
for f, b₃ being FinSequence of Curves T holds
( b₃ = Partial_Sums f iff ( len f = len b₃ & f . 1 = b₃ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₃ . (i + 1) = (b₃ /. 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 b₁ 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;