let n be 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) )
let t be 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) )
let f be Loop of t; ( n >= 2 & rng f = the carrier of (TUnitSphere n) implies ex g being Loop of t st
( g,f are_homotopic & rng g <> the carrier of (TUnitSphere n) ) )
assume that
A1:
n >= 2
and
A2:
rng f = the carrier of (TUnitSphere n)
; ex g being Loop of t st
( g,f are_homotopic & rng g <> the carrier of (TUnitSphere n) )
reconsider n1 = n + 1 as Element of NAT ;
Tunit_circle n1 is SubSpace of TOP-REAL n1
;
then A3:
TUnitSphere n is SubSpace of TOP-REAL n1
by MFOLD_2:def 4;
[#] (Tunit_circle n1) c= [#] (TOP-REAL n1)
by PRE_TOPC:def 4;
then A4:
rng f c= the carrier of (TOP-REAL n1)
by A2, MFOLD_2:def 4;
dom f = the carrier of I[01]
by FUNCT_2:def 1;
then reconsider f1 = f as Function of I[01],(TOP-REAL n1) by A4, FUNCT_2:2;
f1 is continuous
by A3, PRE_TOPC:26;
then consider h being FinSequence of REAL such that
A5:
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Nat
for Q being Subset of I[01]
for W being Subset of (Euclid n1) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = f1 .: Q holds
diameter W < 1 ) )
by JGRAPH_8:1;
set f2 = f * h;
for x being object st x in rng (f * h) holds
x in the carrier of (TUnitSphere n)
;
then consider x being object such that
A6:
( x in the carrier of (TUnitSphere n) & not x in rng (f * h) )
by A1, TARSKI:2;
A7:
[#] (Tunit_circle n1) c= [#] (TOP-REAL n1)
by PRE_TOPC:def 4;
A8:
x in the carrier of (Tunit_circle n1)
by A6, MFOLD_2:def 4;
then reconsider p = x as Point of (TOP-REAL n1) by A7;
p in the carrier of (Tcircle ((0. (TOP-REAL n1)),1))
by A8, TOPREALB:def 7;
then A9:
p in Sphere ((0. (TOP-REAL n1)),1)
by TOPREALB:9;
then A10:
- p in (Sphere ((0. (TOP-REAL n1)),1)) \ {p}
by Th3;
then reconsider U = (TOP-REAL n1) | ((Sphere ((0. (TOP-REAL n1)),1)) \ {p}) as non empty SubSpace of TOP-REAL n1 ;
A11:
[#] U = (Sphere ((0. (TOP-REAL n1)),1)) \ {p}
by PRE_TOPC:def 5;
A12:
- p in Sphere ((0. (TOP-REAL n1)),1)
by A10, XBOOLE_0:def 5;
then A13:
- (- p) in (Sphere ((0. (TOP-REAL n1)),1)) \ {(- p)}
by Th3;
then reconsider V = (TOP-REAL n1) | ((Sphere ((0. (TOP-REAL n1)),1)) \ {(- p)}) as non empty SubSpace of TOP-REAL n1 ;
A14:
[#] V = (Sphere ((0. (TOP-REAL n1)),1)) \ {(- p)}
by PRE_TOPC:def 5;
A15:
for i being Element of NAT st 1 <= i & i < len h & not f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of U holds
f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of V
proof
let i be
Element of
NAT ;
( 1 <= i & i < len h & not f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of U implies f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of V )
assume A16:
( 1
<= i &
i < len h )
;
( f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of U or f .: [.(h /. i),(h /. (i + 1)).] c= the carrier of V )
i in Seg (len h)
by A16, FINSEQ_1:1;
then A17:
i in dom h
by FINSEQ_1:def 3;
reconsider h1 =
h as
real-valued FinSequence ;
reconsider i1 =
i + 1 as
Nat ;
A18:
(
i1 <= len h & 1
<= i1 )
by A16, NAT_1:13;
then
i1 in Seg (len h)
by FINSEQ_1:1;
then A19:
i1 in dom h
by FINSEQ_1:def 3;
h1 . (i + 1) <= 1
by A5, A18, EUCLID_7:7;
then A20:
h /. (i + 1) <= 1
by A19, PARTFUN1:def 6;
h1 . 1
<= h1 . i
by A5, A16, EUCLID_7:7;
then
0 <= h /. i
by A5, A17, PARTFUN1:def 6;
then reconsider Q =
[.(h /. i),(h /. (i + 1)).] as
Subset of
I[01] by A20, BORSUK_1:40, XXREAL_1:34;
f .: Q c= the
carrier of
(TUnitSphere n)
;
then
f .: Q c= [#] (Tunit_circle n1)
by MFOLD_2:def 4;
then
f .: Q c= the
carrier of
(Tcircle ((0. (TOP-REAL n1)),1))
by TOPREALB:def 7;
then A21:
f .: Q c= Sphere (
(0. (TOP-REAL n1)),1)
by TOPREALB:9;
reconsider W =
f1 .: Q as
Subset of
(Euclid n1) by EUCLID:67;
A22:
diameter W < 1
by A16, A5;
Sphere (
(0. (TOP-REAL n1)),1) is
bounded Subset of
(Euclid n1)
by JORDAN2C:11;
then A23:
W is
bounded
by A21, TBSP_1:14;
( not
p in f .: Q or not
- p in f .: Q )
proof
assume A24:
(
p in f .: Q &
- p in f .: Q )
;
contradiction
reconsider p1 =
p,
p2 =
- p as
Point of
(Euclid n1) by EUCLID:67;
A25:
dist (
p1,
p2)
<= diameter W
by A24, A23, TBSP_1:def 8;
A26:
Euclid n1 = MetrStruct(#
(REAL n1),
(Pitag_dist n1) #)
by EUCLID:def 7;
reconsider p3 =
p1,
p4 =
p2 as
Element of
REAL n1 by A26;
reconsider r1 = 1 as
Real ;
dist (
p1,
p2) =
the
distance of
(Euclid n1) . (
p1,
p2)
by METRIC_1:def 1
.=
|.(p3 - p4).|
by A26, EUCLID:def 6
;
then
|.(p - (- p)).| < 1
by A25, A22, XXREAL_0:2;
then
|.(p + (- (- p))).| < 1
;
then
|.((r1 * p) + p).| < 1
by RLVECT_1:def 8;
then
|.((r1 * p) + (r1 * p)).| < 1
by RLVECT_1:def 8;
then
|.((1 + 1) * p).| < 1
by RLVECT_1:def 6;
then A27:
|.2.| * |.p.| < 1
by EUCLID:11;
|.(p - (0. (TOP-REAL n1))).| = 1
by A9, TOPREAL9:9;
then
|.(p + (- (0. (TOP-REAL n1)))).| = 1
;
then
|.(p + ((- 1) * (0. (TOP-REAL n1)))).| = 1
by RLVECT_1:16;
then
|.(p + (0. (TOP-REAL n1))).| = 1
by RLVECT_1:10;
then A28:
|.p.| = 1
by RLVECT_1:4;
|.2.| = 2
by COMPLEX1:43;
hence
contradiction
by A28, A27;
verum
end;
hence
(
f .: [.(h /. i),(h /. (i + 1)).] c= the
carrier of
U or
f .: [.(h /. i),(h /. (i + 1)).] c= the
carrier of
V )
by A14, A11, A21, ZFMISC_1:34;
verum
end;
( f is Path of t,t & t,t are_connected )
;
then reconsider c = f as with_endpoints Curve of (TUnitSphere n) by Th25;
A29:
2 <= len h
by A5, XXREAL_0:2;
A30:
( inf (dom f) = 0 & sup (dom f) = 1 )
by Th4;
then consider fc1 being FinSequence of Curves (TUnitSphere n) such that
A31:
( len fc1 = (len h) - 1 & c = Sum fc1 & ( for i being Nat st 1 <= i & i <= len fc1 holds
fc1 /. i = c | [.(h /. i),(h /. (i + 1)).] ) )
by A5, A29, Th45;
A32:
for i being Nat st 1 <= i & i <= len fc1 & not rng (fc1 /. i) c= the carrier of U holds
rng (fc1 /. i) c= the carrier of V
A35:
for c1 being with_endpoints Curve of (TUnitSphere n) st rng c1 c= the carrier of V & the_first_point_of c1 <> p & the_last_point_of c1 <> p & not inf (dom c1) = sup (dom c1) holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 )
proof
let c1 be
with_endpoints Curve of
(TUnitSphere n);
( rng c1 c= the carrier of V & the_first_point_of c1 <> p & the_last_point_of c1 <> p & not inf (dom c1) = sup (dom c1) implies ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 ) )
assume A36:
rng c1 c= the
carrier of
V
;
( not the_first_point_of c1 <> p or not the_last_point_of c1 <> p or inf (dom c1) = sup (dom c1) or ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 ) )
assume A37:
(
the_first_point_of c1 <> p &
the_last_point_of c1 <> p )
;
( inf (dom c1) = sup (dom c1) or ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 ) )
assume A38:
not
inf (dom c1) = sup (dom c1)
;
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 )
set t1 =
the_first_point_of c1;
set t2 =
the_last_point_of c1;
reconsider p1 =
c1 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) as
Path of
the_first_point_of c1,
the_last_point_of c1 by Th29;
stereographic_projection (
V,
(- p)) is
being_homeomorphism
by A12, A14, MFOLD_2:31;
then A39:
TPlane (
(- p),
(0. (TOP-REAL n1))),
V are_homeomorphic
by T_0TOPSP:def 1;
- p <> 0. (TOP-REAL n1)
then A40:
TOP-REAL n,
TPlane (
(- p),
(0. (TOP-REAL n1)))
are_homeomorphic
by MFOLD_2:29;
then
TOP-REAL n,
V are_homeomorphic
by A39, BORSUK_3:3;
then consider fh being
Function of
(TOP-REAL n),
V such that A41:
fh is
being_homeomorphism
;
A42:
(
dom fh = [#] (TOP-REAL n) &
rng fh = [#] V )
by A41, TOPS_2:58;
A43:
[#] V is
infinite
by A1, A41, A42, CARD_1:59;
reconsider v =
p as
Point of
V by A13, A14;
reconsider S =
([#] V) \ {v} as non
empty Subset of
V by A43, RAMSEY_1:4;
A44:
V | S is
pathwise_connected
by A1, A40, Th10, A39, BORSUK_3:3;
A45:
the_first_point_of c1 in rng c1
by Th31;
A46:
not
the_first_point_of c1 in {v}
by A37, TARSKI:def 1;
A47:
the_last_point_of c1 in rng c1
by Th31;
A48:
not
the_last_point_of c1 in {v}
by A37, TARSKI:def 1;
(
the_first_point_of c1 in S &
the_last_point_of c1 in S )
by A45, A46, A47, A36, A48, XBOOLE_0:def 5;
then
(
the_first_point_of c1 in [#] (V | S) &
the_last_point_of c1 in [#] (V | S) )
by PRE_TOPC:def 5;
then reconsider v1 =
the_first_point_of c1,
v2 =
the_last_point_of c1 as
Point of
(V | S) ;
A49:
v1,
v2 are_connected
by A44;
then consider p3 being
Function of
I[01],
(V | S) such that A50:
(
p3 is
continuous &
p3 . 0 = v1 &
p3 . 1
= v2 )
;
reconsider p3 =
p3 as
Path of
v1,
v2 by A50, A49, BORSUK_2:def 2;
A51:
Tcircle (
(0. (TOP-REAL n1)),1) =
Tunit_circle n1
by TOPREALB:def 7
.=
TUnitSphere n
by MFOLD_2:def 4
;
A52:
V is
SubSpace of
(TOP-REAL n1) | (Sphere ((0. (TOP-REAL n1)),1))
by TOPMETR:22, XBOOLE_1:36;
then A53:
V is
SubSpace of
Tcircle (
(0. (TOP-REAL n1)),1)
by TOPREALB:def 6;
reconsider S0 =
V as non
empty SubSpace of
TUnitSphere n by A51, A52, TOPREALB:def 6;
reconsider s1 =
the_first_point_of c1,
s2 =
the_last_point_of c1 as
Point of
S0 by A45, A47, A36;
A54:
dom p3 = [#] I[01]
by FUNCT_2:def 1;
A55:
[#] S0 c= [#] (TUnitSphere n)
by PRE_TOPC:def 4;
rng p3 c= [#] (V | S)
;
then A56:
rng p3 c= S
by PRE_TOPC:def 5;
then
rng p3 c= [#] S0
by XBOOLE_1:1;
then reconsider p3 =
p3 as
Function of
I[01],
(TUnitSphere n) by A54, A55, FUNCT_2:2, XBOOLE_1:1;
V | S is
SubSpace of
TUnitSphere n
by A53, A51, TSEP_1:7;
then A57:
p3 is
continuous
by A50, PRE_TOPC:26;
then A58:
the_first_point_of c1,
the_last_point_of c1 are_connected
by A50;
then reconsider p2 =
p3 as
Path of
the_first_point_of c1,
the_last_point_of c1 by A50, A57, BORSUK_2:def 2;
rng p1 c= rng c1
by RELAT_1:26;
then A59:
rng p1 c= [#] V
by A36;
A60:
rng p2 c= [#] V
by A56, XBOOLE_1:1;
A61:
s1,
s2 are_connected
by A58, A60, JORDAN:29;
reconsider p5 =
p1,
p6 =
p2 as
Path of
s1,
s2 by A58, A60, A59, JORDAN:29;
reconsider n0 =
n as
Element of
NAT by ORDINAL1:def 12;
S0 is
simply_connected
by Th14, A39;
then
Class (
(EqRel (S0,s1,s2)),
p5)
= Class (
(EqRel (S0,s1,s2)),
p6)
by Th12;
then
p5,
p6 are_homotopic
by A61, TOPALG_1:46;
then A62:
p1,
p2 are_homotopic
by A58, A61, Th6;
set r1 =
inf (dom c1);
set r2 =
sup (dom c1);
A63:
inf (dom c1) <= sup (dom c1)
by XXREAL_2:40;
then A64:
inf (dom c1) < sup (dom c1)
by A38, XXREAL_0:1;
then reconsider c2 =
p2 * (L[01] ((inf (dom c1)),(sup (dom c1)),0,1)) as
with_endpoints Curve of
(TUnitSphere n) by A58, Th32;
take
c2
;
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 )
rng (L[01] ((inf (dom c1)),(sup (dom c1)),0,1)) c= [#] (Closed-Interval-TSpace (0,1))
by RELAT_1:def 19;
then
rng (L[01] ((inf (dom c1)),(sup (dom c1)),0,1)) c= dom p2
by FUNCT_2:def 1, TOPMETR:20;
then
dom c2 = dom (L[01] ((inf (dom c1)),(sup (dom c1)),0,1))
by RELAT_1:27;
then
dom c2 = [#] (Closed-Interval-TSpace ((inf (dom c1)),(sup (dom c1))))
by FUNCT_2:def 1;
then A65:
dom c2 = [.(inf (dom c1)),(sup (dom c1)).]
by A63, TOPMETR:18;
A66:
c2 * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))) =
p2 * ((L[01] ((inf (dom c1)),(sup (dom c1)),0,1)) * (L[01] (0,1,(inf (dom c1)),(sup (dom c1)))))
by RELAT_1:36
.=
p2 * (id (Closed-Interval-TSpace (0,1)))
by Th1, A64, Th2
.=
p2
by FUNCT_2:17, TOPMETR:20
;
(
inf (dom c1) = inf (dom c2) &
sup (dom c1) = sup (dom c2) )
by A65, Th27;
hence
c1,
c2 are_homotopic
by A62, A66;
( rng c2 c= the carrier of U & dom c1 = dom c2 )
A67:
rng c2 c= rng p2
by RELAT_1:26;
A68:
((Sphere ((0. (TOP-REAL n1)),1)) \ {p}) \ {(- p)} c= (Sphere ((0. (TOP-REAL n1)),1)) \ {p}
by XBOOLE_1:36;
rng c2 c= ([#] V) \ {p}
by A56, A67;
then
rng c2 c= (Sphere ((0. (TOP-REAL n1)),1)) \ ({(- p)} \/ {p})
by A14, XBOOLE_1:41;
then
rng c2 c= ((Sphere ((0. (TOP-REAL n1)),1)) \ {p}) \ {(- p)}
by XBOOLE_1:41;
hence
rng c2 c= the
carrier of
U
by A11, A68;
dom c1 = dom c2
thus
dom c1 = dom c2
by A65, Th27;
verum
end;
A69:
for i being Nat st 1 <= i & i <= len fc1 holds
( i + 1 in dom h & i in dom h & dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).] & h /. i < h /. (i + 1) )
proof
let i be
Nat;
( 1 <= i & i <= len fc1 implies ( i + 1 in dom h & i in dom h & dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).] & h /. i < h /. (i + 1) ) )
assume A70:
( 1
<= i &
i <= len fc1 )
;
( i + 1 in dom h & i in dom h & dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).] & h /. i < h /. (i + 1) )
A71:
1
<= 1
+ i
by NAT_1:11;
A72:
i + 1
<= ((len h) - 1) + 1
by A70, A31, XREAL_1:6;
then
i + 1
in Seg (len h)
by A71, FINSEQ_1:1;
hence A73:
i + 1
in dom h
by FINSEQ_1:def 3;
( i in dom h & dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).] & h /. i < h /. (i + 1) )
A74:
i < i + 1
by NAT_1:13;
i <= len h
by A72, NAT_1:13;
then
i in Seg (len h)
by A70, FINSEQ_1:1;
hence A75:
i in dom h
by FINSEQ_1:def 3;
( dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).] & h /. i < h /. (i + 1) )
A76:
h /. i = h . i
by A75, PARTFUN1:def 6;
A77:
h /. (i + 1) = h . (i + 1)
by A73, PARTFUN1:def 6;
A78:
0 <= h . i
A80:
h . (i + 1) <= 1
[.(h . i),(h . (i + 1)).] c= [.0,1.]
by A78, A80, XXREAL_1:34;
then A83:
[.(h . i),(h . (i + 1)).] c= dom c
by A30, Th27;
A84:
fc1 /. i = c | [.(h /. i),(h /. (i + 1)).]
by A31, A70;
thus
dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).]
by A84, A83, A76, A77, RELAT_1:62;
h /. i < h /. (i + 1)
thus
h /. i < h /. (i + 1)
by A77, A76, A75, A73, A74, A5, VALUED_0:def 13;
verum
end;
A85:
for i being Nat st 1 <= i & i <= len fc1 holds
( fc1 /. i is with_endpoints & ( for c1 being with_endpoints Curve of (TUnitSphere n) st c1 = fc1 /. i holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] ) ) )
proof
let i be
Nat;
( 1 <= i & i <= len fc1 implies ( fc1 /. i is with_endpoints & ( for c1 being with_endpoints Curve of (TUnitSphere n) st c1 = fc1 /. i holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] ) ) ) )
assume A86:
( 1
<= i &
i <= len fc1 )
;
( fc1 /. i is with_endpoints & ( for c1 being with_endpoints Curve of (TUnitSphere n) st c1 = fc1 /. i holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] ) ) )
A87:
fc1 /. i = c | [.(h /. i),(h /. (i + 1)).]
by A31, A86;
A88:
i + 1
in dom h
by A69, A86;
A89:
i in dom h
by A69, A86;
A90:
i < i + 1
by NAT_1:13;
A91:
h . i < h . (i + 1)
by A89, A88, A90, A5, VALUED_0:def 13;
A92:
dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).]
by A69, A86;
h /. i < h /. (i + 1)
by A69, A86;
then
(
dom (fc1 /. i) is
left_end &
dom (fc1 /. i) is
right_end )
by A92, XXREAL_2:33;
then
(
fc1 /. i is
with_first_point &
fc1 /. i is
with_last_point )
;
hence
fc1 /. i is
with_endpoints
;
for c1 being with_endpoints Curve of (TUnitSphere n) st c1 = fc1 /. i holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] )
let c1 be
with_endpoints Curve of
(TUnitSphere n);
( c1 = fc1 /. i implies ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] ) )
assume A93:
c1 = fc1 /. i
;
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] )
A94:
dom c1 = [.(inf (dom c1)),(sup (dom c1)).]
by Th27;
A95:
inf (dom c1) <= sup (dom c1)
by XXREAL_2:40;
A96:
inf (dom c1) = h /. i
by A93, A94, A95, A92, XXREAL_1:66;
A97:
h /. i = h . i
by A89, PARTFUN1:def 6;
A98:
sup (dom c1) = h /. (i + 1)
by A93, A94, A95, A92, XXREAL_1:66;
A99:
h /. (i + 1) = h . (i + 1)
by A88, PARTFUN1:def 6;
per cases
( rng c1 c= the carrier of U or rng c1 c= the carrier of V )
by A32, A86, A93;
suppose A101:
rng c1 c= the
carrier of
V
;
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] )A102:
rng h c= dom f
by A5, FUNCT_2:def 1;
then A103:
dom (f * h) = dom h
by RELAT_1:27;
A104:
i + 1
in dom (f * h)
by A102, A88, RELAT_1:27;
A105:
the_first_point_of c1 <> p
proof
assume A106:
the_first_point_of c1 = p
;
contradiction
inf (dom c1) in dom c1
by A94, A95, XXREAL_1:1;
then c1 . (inf (dom c1)) =
f . (h . i)
by A96, A97, A93, A87, FUNCT_1:47
.=
(f * h) . i
by A103, A89, FUNCT_1:12
;
hence
contradiction
by A6, A106, A103, A89, FUNCT_1:3;
verum
end; A107:
the_last_point_of c1 <> p
proof
assume A108:
the_last_point_of c1 = p
;
contradiction
sup (dom c1) in dom c1
by A94, A95, XXREAL_1:1;
then c1 . (sup (dom c1)) =
f . (h . (i + 1))
by A98, A99, A93, A87, FUNCT_1:47
.=
(f * h) . (i + 1)
by A104, FUNCT_1:12
;
hence
contradiction
by A6, A108, A104, FUNCT_1:3;
verum
end; consider c2 being
with_endpoints Curve of
(TUnitSphere n) such that A109:
(
c1,
c2 are_homotopic &
rng c2 c= the
carrier of
U &
dom c1 = dom c2 )
by A35, A101, A105, A107, A96, A98, A91, A97, A99;
take
c2
;
( c1,c2 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] )thus
(
c1,
c2 are_homotopic &
rng c2 c= the
carrier of
U &
dom c1 = dom c2 &
dom c1 = [.(h /. i),(h /. (i + 1)).] )
by A109, A93, A69, A86;
verum end;
end;
defpred S1[ set , set ] means for i being Nat
for c1 being with_endpoints Curve of (TUnitSphere n) st i = $1 & c1 = fc1 /. i holds
ex c2 being with_endpoints Curve of (TUnitSphere n) st
( c2 = $2 & c2,c1 are_homotopic & rng c2 c= the carrier of U & dom c1 = dom c2 & dom c1 = [.(h /. i),(h /. (i + 1)).] );
A110:
for k being Nat st k in Seg (len fc1) holds
ex x being Element of Curves (TUnitSphere n) st S1[k,x]
ex p being FinSequence of Curves (TUnitSphere n) st
( dom p = Seg (len fc1) & ( for k being Nat st k in Seg (len fc1) holds
S1[k,p . k] ) )
from FINSEQ_1:sch 5(A110);
then consider fc2 being FinSequence of Curves (TUnitSphere n) such that
A113:
( dom fc2 = Seg (len fc1) & ( for k being Nat st k in Seg (len fc1) holds
S1[k,fc2 . k] ) )
;
A114:
len fc2 = len fc1
by A113, FINSEQ_1:def 3;
A115:
2 - 1 <= (len h) - 1
by A29, XREAL_1:9;
then A116:
len fc2 > 0
by A31, A113, FINSEQ_1:def 3;
A117:
for i being Nat st 1 <= i & i < len fc2 holds
( (fc2 /. i) . (sup (dom (fc2 /. i))) = (fc2 /. (i + 1)) . (inf (dom (fc2 /. (i + 1)))) & sup (dom (fc2 /. i)) = inf (dom (fc2 /. (i + 1))) )
proof
let i be
Nat;
( 1 <= i & i < len fc2 implies ( (fc2 /. i) . (sup (dom (fc2 /. i))) = (fc2 /. (i + 1)) . (inf (dom (fc2 /. (i + 1)))) & sup (dom (fc2 /. i)) = inf (dom (fc2 /. (i + 1))) ) )
assume A118:
( 1
<= i &
i < len fc2 )
;
( (fc2 /. i) . (sup (dom (fc2 /. i))) = (fc2 /. (i + 1)) . (inf (dom (fc2 /. (i + 1)))) & sup (dom (fc2 /. i)) = inf (dom (fc2 /. (i + 1))) )
then
( 1
<= i &
i <= len fc1 )
by A113, FINSEQ_1:def 3;
then A119:
i in Seg (len fc1)
by FINSEQ_1:1;
set ci =
fc1 /. i;
reconsider ci =
fc1 /. i as
with_endpoints Curve of
(TUnitSphere n) by A118, A114, A85;
consider di being
with_endpoints Curve of
(TUnitSphere n) such that A120:
(
di = fc2 . i &
di,
ci are_homotopic &
rng di c= the
carrier of
U &
dom ci = dom di &
dom ci = [.(h /. i),(h /. (i + 1)).] )
by A119, A113;
1
+ 1
<= i + 1
by A118, XREAL_1:6;
then A121:
1
<= i + 1
by XXREAL_0:2;
A122:
i + 1
<= len fc2
by A118, NAT_1:13;
then A123:
i + 1
in Seg (len fc1)
by A114, A121, FINSEQ_1:1;
set ci1 =
fc1 /. (i + 1);
reconsider ci1 =
fc1 /. (i + 1) as
with_endpoints Curve of
(TUnitSphere n) by A121, A122, A114, A85;
consider di1 being
with_endpoints Curve of
(TUnitSphere n) such that A124:
(
di1 = fc2 . (i + 1) &
di1,
ci1 are_homotopic &
rng di1 c= the
carrier of
U &
dom ci1 = dom di1 &
dom ci1 = [.(h /. (i + 1)),(h /. ((i + 1) + 1)).] )
by A123, A113;
A125:
i + 1
in dom fc2
by A122, A113, A114, A121, FINSEQ_1:1;
A126:
h /. i < h /. (i + 1)
by A69, A118, A114;
A127:
h /. (i + 1) < h /. ((i + 1) + 1)
by A69, A121, A122, A114;
A128:
dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).]
by A69, A118, A114;
A129:
dom (fc1 /. (i + 1)) = [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]
by A69, A121, A122, A114;
A130:
h /. (i + 1) in [.(h /. i),(h /. (i + 1)).]
by A126, XXREAL_1:1;
A131:
h /. (i + 1) in [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]
by A127, XXREAL_1:1;
A132:
fc2 /. i = fc2 . i
by A119, A113, PARTFUN1:def 6;
A133:
fc2 /. (i + 1) = fc2 . (i + 1)
by A125, PARTFUN1:def 6;
thus (fc2 /. i) . (sup (dom (fc2 /. i))) =
the_last_point_of di
by A120, A132
.=
the_last_point_of ci
by A120, Th35
.=
(fc1 /. i) . (h /. (i + 1))
by A126, A128, XXREAL_2:29
.=
(c | [.(h /. i),(h /. (i + 1)).]) . (h /. (i + 1))
by A31, A118, A114
.=
c . (h /. (i + 1))
by A130, FUNCT_1:49
.=
(c | [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]) . (h /. (i + 1))
by A131, FUNCT_1:49
.=
(fc1 /. (i + 1)) . (h /. (i + 1))
by A31, A121, A122, A114
.=
the_first_point_of ci1
by A127, A129, XXREAL_2:25
.=
the_first_point_of di1
by A124, Th35
.=
(fc2 /. (i + 1)) . (inf (dom (fc2 /. (i + 1))))
by A124, A133
;
sup (dom (fc2 /. i)) = inf (dom (fc2 /. (i + 1)))
A134:
dom (fc2 /. i) = [.(h /. i),(h /. (i + 1)).]
by A120, A119, A113, PARTFUN1:def 6;
A135:
dom (fc2 /. (i + 1)) = [.(h /. (i + 1)),(h /. (i + 2)).]
by A124, A125, PARTFUN1:def 6;
thus sup (dom (fc2 /. i)) =
h /. (i + 1)
by A134, A126, XXREAL_2:29
.=
inf (dom (fc2 /. (i + 1)))
by A135, A127, XXREAL_2:25
;
verum
end;
A136:
for i being Nat st 1 <= i & i <= len fc2 holds
fc2 /. i is with_endpoints
consider c0 being with_endpoints Curve of (TUnitSphere n) such that
A140:
( Sum fc2 = c0 & dom c0 = [.(inf (dom (fc2 /. 1))),(sup (dom (fc2 /. (len fc2)))).] & the_first_point_of c0 = (fc2 /. 1) . (inf (dom (fc2 /. 1))) & the_last_point_of c0 = (fc2 /. (len fc2)) . (sup (dom (fc2 /. (len fc2)))) )
by A117, A136, A116, Th43;
A141:
for i being Nat st 1 <= i & i < len fc1 holds
( (fc1 /. i) . (sup (dom (fc1 /. i))) = (fc1 /. (i + 1)) . (inf (dom (fc1 /. (i + 1)))) & sup (dom (fc1 /. i)) = inf (dom (fc1 /. (i + 1))) )
proof
let i be
Nat;
( 1 <= i & i < len fc1 implies ( (fc1 /. i) . (sup (dom (fc1 /. i))) = (fc1 /. (i + 1)) . (inf (dom (fc1 /. (i + 1)))) & sup (dom (fc1 /. i)) = inf (dom (fc1 /. (i + 1))) ) )
assume A142:
( 1
<= i &
i < len fc1 )
;
( (fc1 /. i) . (sup (dom (fc1 /. i))) = (fc1 /. (i + 1)) . (inf (dom (fc1 /. (i + 1)))) & sup (dom (fc1 /. i)) = inf (dom (fc1 /. (i + 1))) )
A143:
i in Seg (len fc1)
by A142, FINSEQ_1:1;
set ci =
fc1 /. i;
reconsider ci =
fc1 /. i as
with_endpoints Curve of
(TUnitSphere n) by A142, A85;
consider di being
with_endpoints Curve of
(TUnitSphere n) such that A144:
(
di = fc2 . i &
di,
ci are_homotopic &
rng di c= the
carrier of
U &
dom ci = dom di &
dom ci = [.(h /. i),(h /. (i + 1)).] )
by A143, A113;
1
+ 1
<= i + 1
by A142, XREAL_1:6;
then A145:
1
<= i + 1
by XXREAL_0:2;
A146:
i + 1
<= len fc2
by A114, A142, NAT_1:13;
then A147:
i + 1
in Seg (len fc1)
by A114, A145, FINSEQ_1:1;
set ci1 =
fc1 /. (i + 1);
reconsider ci1 =
fc1 /. (i + 1) as
with_endpoints Curve of
(TUnitSphere n) by A145, A146, A114, A85;
consider di1 being
with_endpoints Curve of
(TUnitSphere n) such that A148:
(
di1 = fc2 . (i + 1) &
di1,
ci1 are_homotopic &
rng di1 c= the
carrier of
U &
dom ci1 = dom di1 &
dom ci1 = [.(h /. (i + 1)),(h /. ((i + 1) + 1)).] )
by A147, A113;
A149:
h /. i < h /. (i + 1)
by A69, A142;
A150:
h /. (i + 1) < h /. ((i + 1) + 1)
by A69, A145, A146, A114;
A151:
dom (fc1 /. i) = [.(h /. i),(h /. (i + 1)).]
by A69, A142;
A152:
dom (fc1 /. (i + 1)) = [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]
by A69, A145, A146, A114;
A153:
h /. (i + 1) in [.(h /. i),(h /. (i + 1)).]
by A149, XXREAL_1:1;
A154:
h /. (i + 1) in [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]
by A150, XXREAL_1:1;
thus (fc1 /. i) . (sup (dom (fc1 /. i))) =
(fc1 /. i) . (h /. (i + 1))
by A149, A151, XXREAL_2:29
.=
(c | [.(h /. i),(h /. (i + 1)).]) . (h /. (i + 1))
by A31, A142
.=
c . (h /. (i + 1))
by A153, FUNCT_1:49
.=
(c | [.(h /. (i + 1)),(h /. ((i + 1) + 1)).]) . (h /. (i + 1))
by A154, FUNCT_1:49
.=
(fc1 /. (i + 1)) . (h /. (i + 1))
by A31, A145, A146, A114
.=
(fc1 /. (i + 1)) . (inf (dom (fc1 /. (i + 1))))
by A150, A152, XXREAL_2:25
;
sup (dom (fc1 /. i)) = inf (dom (fc1 /. (i + 1)))
thus sup (dom (fc1 /. i)) =
h /. (i + 1)
by A144, A149, XXREAL_2:29
.=
inf (dom (fc1 /. (i + 1)))
by A148, A150, XXREAL_2:25
;
verum
end;
for i being Nat st 1 <= i & i <= len fc2 holds
ex c3, c4 being with_endpoints Curve of (TUnitSphere n) st
( c3 = fc2 /. i & c4 = fc1 /. i & c3,c4 are_homotopic & dom c3 = dom c4 )
proof
let i be
Nat;
( 1 <= i & i <= len fc2 implies ex c3, c4 being with_endpoints Curve of (TUnitSphere n) st
( c3 = fc2 /. i & c4 = fc1 /. i & c3,c4 are_homotopic & dom c3 = dom c4 ) )
assume A155:
( 1
<= i &
i <= len fc2 )
;
ex c3, c4 being with_endpoints Curve of (TUnitSphere n) st
( c3 = fc2 /. i & c4 = fc1 /. i & c3,c4 are_homotopic & dom c3 = dom c4 )
then A156:
i in Seg (len fc1)
by A114, FINSEQ_1:1;
set ci =
fc1 /. i;
reconsider ci =
fc1 /. i as
with_endpoints Curve of
(TUnitSphere n) by A155, A114, A85;
consider di being
with_endpoints Curve of
(TUnitSphere n) such that A157:
(
di = fc2 . i &
di,
ci are_homotopic &
rng di c= the
carrier of
U &
dom ci = dom di &
dom ci = [.(h /. i),(h /. (i + 1)).] )
by A156, A113;
A158:
i in dom fc2
by A155, A114, A113, FINSEQ_1:1;
take
di
;
ex c4 being with_endpoints Curve of (TUnitSphere n) st
( di = fc2 /. i & c4 = fc1 /. i & di,c4 are_homotopic & dom di = dom c4 )
take
ci
;
( di = fc2 /. i & ci = fc1 /. i & di,ci are_homotopic & dom di = dom ci )
thus
(
di = fc2 /. i &
ci = fc1 /. i &
di,
ci are_homotopic &
dom di = dom ci )
by A157, A158, PARTFUN1:def 6;
verum
end;
then A159:
c0,c are_homotopic
by A117, A141, A140, Th44, A114, A115, A31;
A160:
dom c0 = [.0,1.]
proof
A161:
0 + 1
< (len fc1) + 1
by A115, A31, XREAL_1:6;
A162:
1
in Seg (len fc1)
by A115, A31, FINSEQ_1:1;
set ci =
fc1 /. 1;
reconsider ci =
fc1 /. 1 as
with_endpoints Curve of
(TUnitSphere n) by A115, A31, A85;
consider di being
with_endpoints Curve of
(TUnitSphere n) such that A163:
(
di = fc2 . 1 &
di,
ci are_homotopic &
rng di c= the
carrier of
U &
dom ci = dom di &
dom ci = [.(h /. 1),(h /. (1 + 1)).] )
by A162, A113;
1
in Seg (len fc2)
by A115, A31, A114, FINSEQ_1:1;
then
1
in dom fc2
by FINSEQ_1:def 3;
then A164:
dom (fc2 /. 1) = [.(h /. 1),(h /. (1 + 1)).]
by A163, PARTFUN1:def 6;
A165:
h /. 1
< h /. (1 + 1)
by A69, A115, A31;
1
in Seg (len h)
by A161, A31, FINSEQ_1:1;
then A166:
1
in dom h
by FINSEQ_1:def 3;
A167:
inf (dom (fc2 /. 1)) =
h /. 1
by A165, A164, XXREAL_2:25
.=
0
by A5, A166, PARTFUN1:def 6
;
A168:
len fc1 in Seg (len fc1)
by A115, A31, FINSEQ_1:1;
set ci1 =
fc1 /. (len fc1);
reconsider ci1 =
fc1 /. (len fc1) as
with_endpoints Curve of
(TUnitSphere n) by A115, A31, A85;
consider di1 being
with_endpoints Curve of
(TUnitSphere n) such that A169:
(
di1 = fc2 . (len fc1) &
di1,
ci1 are_homotopic &
rng di1 c= the
carrier of
U &
dom ci1 = dom di1 &
dom ci1 = [.(h /. (len fc1)),(h /. ((len fc1) + 1)).] )
by A168, A113;
len fc1 in Seg (len fc2)
by A114, A115, A31, FINSEQ_1:1;
then
len fc1 in dom fc2
by FINSEQ_1:def 3;
then A170:
dom (fc2 /. (len fc2)) = [.(h /. (len fc1)),(h /. ((len fc1) + 1)).]
by A169, A114, PARTFUN1:def 6;
A171:
h /. (len fc1) < h /. ((len fc1) + 1)
by A69, A115, A31;
len h in Seg (len h)
by A161, A31, FINSEQ_1:1;
then A172:
len h in dom h
by FINSEQ_1:def 3;
A173:
sup (dom (fc2 /. (len fc2))) =
h /. ((len fc1) + 1)
by A171, A170, XXREAL_2:29
.=
1
by A5, A31, A172, PARTFUN1:def 6
;
thus
dom c0 = [.0,1.]
by A140, A167, A173;
verum
end;
for i being Nat st 1 <= i & i <= len fc2 holds
rng (fc2 /. i) c= the carrier of U
then A178:
rng c0 c= the carrier of U
by A140, Th42;
A179:
t,t are_connected
;
A180: t =
the_first_point_of c
by A30, A179, BORSUK_2:def 2
.=
the_first_point_of c0
by Th35, A159
;
A181: t =
the_last_point_of c
by A30, A179, BORSUK_2:def 2
.=
the_last_point_of c0
by Th35, A159
;
reconsider f0 = c0 as Loop of t by A160, A180, A181, Th28;
A182:
f0,f are_homotopic
by A159, A179, Th34;
not p in rng f0
hence
ex g being Loop of t st
( g,f are_homotopic & rng g <> the carrier of (TUnitSphere n) )
by A6, A182; verum