let T be 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
defpred S1[ Nat] means for f1, f2 being FinSequence of Curves T
for c1, c2 being with_endpoints Curve of T st len f1 = $1 & 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 ;
A1:
S1[ 0 ]
;
A2:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A3:
S1[
k]
;
S1[k + 1]
let f1,
f2 be
FinSequence of
Curves T;
for c1, c2 being with_endpoints Curve of T st len f1 = k + 1 & 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 let c1,
c2 be
with_endpoints Curve of
T;
( len f1 = k + 1 & 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 ) ) implies c1,c2 are_homotopic )
assume A4:
(
len f1 = k + 1 &
len f1 > 0 )
;
( not len f1 = len f2 or not Sum f1 = c1 or not Sum f2 = c2 or ex i being Nat st
( 1 <= i & i < len f1 & not ( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i < len f2 & not ( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i <= len f1 & ( for c3, c4 being with_endpoints Curve of T holds
( not c3 = f1 /. i or not c4 = f2 /. i or not c3,c4 are_homotopic or not dom c3 = dom c4 ) ) ) or c1,c2 are_homotopic )
consider f1a being
FinSequence of
Curves T,
c1b being
Element of
Curves T such that A5:
f1 = f1a ^ <*c1b*>
by A4, FINSEQ_2:19;
A6:
len f1 =
(len f1a) + (len <*c1b*>)
by A5, FINSEQ_1:22
.=
(len f1a) + 1
by FINSEQ_1:39
;
assume A7:
len f1 = len f2
;
( not Sum f1 = c1 or not Sum f2 = c2 or ex i being Nat st
( 1 <= i & i < len f1 & not ( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i < len f2 & not ( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i <= len f1 & ( for c3, c4 being with_endpoints Curve of T holds
( not c3 = f1 /. i or not c4 = f2 /. i or not c3,c4 are_homotopic or not dom c3 = dom c4 ) ) ) or c1,c2 are_homotopic )
consider f2a being
FinSequence of
Curves T,
c2b being
Element of
Curves T such that A8:
f2 = f2a ^ <*c2b*>
by A7, A4, FINSEQ_2:19;
A9:
len f2 =
(len f2a) + (len <*c2b*>)
by A8, FINSEQ_1:22
.=
(len f2a) + 1
by FINSEQ_1:39
;
assume A10:
(
Sum f1 = c1 &
Sum f2 = c2 )
;
( ex i being Nat st
( 1 <= i & i < len f1 & not ( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i < len f2 & not ( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i <= len f1 & ( for c3, c4 being with_endpoints Curve of T holds
( not c3 = f1 /. i or not c4 = f2 /. i or not c3,c4 are_homotopic or not dom c3 = dom c4 ) ) ) or c1,c2 are_homotopic )
assume A11:
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))) )
;
( ex i being Nat st
( 1 <= i & i < len f2 & not ( (f2 /. i) . (sup (dom (f2 /. i))) = (f2 /. (i + 1)) . (inf (dom (f2 /. (i + 1)))) & sup (dom (f2 /. i)) = inf (dom (f2 /. (i + 1))) ) ) or ex i being Nat st
( 1 <= i & i <= len f1 & ( for c3, c4 being with_endpoints Curve of T holds
( not c3 = f1 /. i or not c4 = f2 /. i or not c3,c4 are_homotopic or not dom c3 = dom c4 ) ) ) or c1,c2 are_homotopic )
assume A12:
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))) )
;
( ex i being Nat st
( 1 <= i & i <= len f1 & ( for c3, c4 being with_endpoints Curve of T holds
( not c3 = f1 /. i or not c4 = f2 /. i or not c3,c4 are_homotopic or not dom c3 = dom c4 ) ) ) or c1,c2 are_homotopic )
assume A13:
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 )
;
c1,c2 are_homotopic
A14:
dom f1 =
Seg (len f1)
by FINSEQ_1:def 3
.=
dom f2
by A7, FINSEQ_1:def 3
;
A15:
1
<= len f1
by A4, NAT_1:11;
then
len f1 in Seg (len f1)
by FINSEQ_1:1;
then A16:
len f1 in dom f1
by FINSEQ_1:def 3;
then A17:
f1 /. (len f1) = f1 . (len f1)
by PARTFUN1:def 6;
consider c1bb,
c2bb being
with_endpoints Curve of
T such that A18:
(
c1bb = f1 /. (len f1) &
c2bb = f2 /. (len f1) &
c1bb,
c2bb are_homotopic &
dom c1bb = dom c2bb )
by A13, A15;
A19:
f1 . (len f1) = c1b
by A5, A6, FINSEQ_1:42;
A20:
f2 . (len f2) = c2b
by A8, A9, FINSEQ_1:42;
A21:
(
c1bb = c1b &
c2bb = c2b )
by A7, A16, A14, A18, A19, A20, PARTFUN1:def 6;
reconsider c1b =
c1b,
c2b =
c2b as
with_endpoints Curve of
T by A7, A20, A18, A14, A16, A17, A5, A6, FINSEQ_1:42, PARTFUN1:def 6;
per cases
( len f1a > 0 or not len f1a > 0 )
;
suppose A22:
len f1a > 0
;
c1,c2 are_homotopic A23:
for
i being
Nat st 1
<= i &
i < len f1a holds
(
(f1a /. i) . (sup (dom (f1a /. i))) = (f1a /. (i + 1)) . (inf (dom (f1a /. (i + 1)))) &
sup (dom (f1a /. i)) = inf (dom (f1a /. (i + 1))) )
proof
let i be
Nat;
( 1 <= i & i < len f1a implies ( (f1a /. i) . (sup (dom (f1a /. i))) = (f1a /. (i + 1)) . (inf (dom (f1a /. (i + 1)))) & sup (dom (f1a /. i)) = inf (dom (f1a /. (i + 1))) ) )
assume A24:
( 1
<= i &
i < len f1a )
;
( (f1a /. i) . (sup (dom (f1a /. i))) = (f1a /. (i + 1)) . (inf (dom (f1a /. (i + 1)))) & sup (dom (f1a /. i)) = inf (dom (f1a /. (i + 1))) )
then A25:
i + 1
< (len f1a) + 1
by XREAL_1:6;
i <= i + 1
by NAT_1:11;
then A26:
i < len f1
by A6, A25, XXREAL_0:2;
i in Seg (len f1)
by A24, A26, FINSEQ_1:1;
then A27:
i in dom f1
by FINSEQ_1:def 3;
i in Seg (len f1a)
by A24, FINSEQ_1:1;
then A28:
i in dom f1a
by FINSEQ_1:def 3;
A29:
f1 /. i =
f1 . i
by A27, PARTFUN1:def 6
.=
f1a . i
by A28, A5, FINSEQ_1:def 7
.=
f1a /. i
by A28, PARTFUN1:def 6
;
A30:
1
<= i + 1
by NAT_1:11;
i + 1
in Seg (len f1)
by A30, A25, A6, FINSEQ_1:1;
then A31:
i + 1
in dom f1
by FINSEQ_1:def 3;
i + 1
<= len f1a
by A24, NAT_1:13;
then
i + 1
in Seg (len f1a)
by A30, FINSEQ_1:1;
then A32:
i + 1
in dom f1a
by FINSEQ_1:def 3;
f1 /. (i + 1) =
f1 . (i + 1)
by A31, PARTFUN1:def 6
.=
f1a . (i + 1)
by A32, A5, FINSEQ_1:def 7
.=
f1a /. (i + 1)
by A32, PARTFUN1:def 6
;
hence
(
(f1a /. i) . (sup (dom (f1a /. i))) = (f1a /. (i + 1)) . (inf (dom (f1a /. (i + 1)))) &
sup (dom (f1a /. i)) = inf (dom (f1a /. (i + 1))) )
by A26, A29, A24, A11;
verum
end;
for
i being
Nat st 1
<= i &
i <= len f1a holds
f1a /. i is
with_endpoints
proof
let i be
Nat;
( 1 <= i & i <= len f1a implies f1a /. i is with_endpoints )
assume A33:
( 1
<= i &
i <= len f1a )
;
f1a /. i is with_endpoints
then A34:
i + 1
<= (len f1a) + 1
by XREAL_1:6;
i <= i + 1
by NAT_1:11;
then A35:
i <= len f1
by A6, A34, XXREAL_0:2;
i in Seg (len f1)
by A33, A35, FINSEQ_1:1;
then A36:
i in dom f1
by FINSEQ_1:def 3;
i in Seg (len f1a)
by A33, FINSEQ_1:1;
then A37:
i in dom f1a
by FINSEQ_1:def 3;
A38:
ex
c3,
c4 being
with_endpoints Curve of
T st
(
c3 = f1 /. i &
c4 = f2 /. i &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A33, A35, A13;
f1 /. i =
f1 . i
by A36, PARTFUN1:def 6
.=
f1a . i
by A37, A5, FINSEQ_1:def 7
.=
f1a /. i
by A37, PARTFUN1:def 6
;
hence
f1a /. i is
with_endpoints
by A38;
verum
end; then consider c1a being
with_endpoints Curve of
T such that A39:
(
Sum f1a = c1a &
dom c1a = [.(inf (dom (f1a /. 1))),(sup (dom (f1a /. (len f1a)))).] &
the_first_point_of c1a = (f1a /. 1) . (inf (dom (f1a /. 1))) &
the_last_point_of c1a = (f1a /. (len f1a)) . (sup (dom (f1a /. (len f1a)))) )
by A22, A23, Th43;
A40:
for
i being
Nat st 1
<= i &
i < len f2a holds
(
(f2a /. i) . (sup (dom (f2a /. i))) = (f2a /. (i + 1)) . (inf (dom (f2a /. (i + 1)))) &
sup (dom (f2a /. i)) = inf (dom (f2a /. (i + 1))) )
proof
let i be
Nat;
( 1 <= i & i < len f2a implies ( (f2a /. i) . (sup (dom (f2a /. i))) = (f2a /. (i + 1)) . (inf (dom (f2a /. (i + 1)))) & sup (dom (f2a /. i)) = inf (dom (f2a /. (i + 1))) ) )
assume A41:
( 1
<= i &
i < len f2a )
;
( (f2a /. i) . (sup (dom (f2a /. i))) = (f2a /. (i + 1)) . (inf (dom (f2a /. (i + 1)))) & sup (dom (f2a /. i)) = inf (dom (f2a /. (i + 1))) )
then A42:
i + 1
< (len f2a) + 1
by XREAL_1:6;
i <= i + 1
by NAT_1:11;
then A43:
i < len f2
by A9, A42, XXREAL_0:2;
i in Seg (len f2)
by A41, A43, FINSEQ_1:1;
then A44:
i in dom f2
by FINSEQ_1:def 3;
i in Seg (len f2a)
by A41, FINSEQ_1:1;
then A45:
i in dom f2a
by FINSEQ_1:def 3;
A46:
f2 /. i =
f2 . i
by A44, PARTFUN1:def 6
.=
f2a . i
by A45, A8, FINSEQ_1:def 7
.=
f2a /. i
by A45, PARTFUN1:def 6
;
A47:
1
<= i + 1
by NAT_1:11;
i + 1
in Seg (len f2)
by A47, A42, A9, FINSEQ_1:1;
then A48:
i + 1
in dom f2
by FINSEQ_1:def 3;
i + 1
<= len f2a
by A41, NAT_1:13;
then
i + 1
in Seg (len f2a)
by A47, FINSEQ_1:1;
then A49:
i + 1
in dom f2a
by FINSEQ_1:def 3;
f2 /. (i + 1) =
f2 . (i + 1)
by A48, PARTFUN1:def 6
.=
f2a . (i + 1)
by A49, A8, FINSEQ_1:def 7
.=
f2a /. (i + 1)
by A49, PARTFUN1:def 6
;
hence
(
(f2a /. i) . (sup (dom (f2a /. i))) = (f2a /. (i + 1)) . (inf (dom (f2a /. (i + 1)))) &
sup (dom (f2a /. i)) = inf (dom (f2a /. (i + 1))) )
by A43, A46, A41, A12;
verum
end;
for
i being
Nat st 1
<= i &
i <= len f2a holds
f2a /. i is
with_endpoints
proof
let i be
Nat;
( 1 <= i & i <= len f2a implies f2a /. i is with_endpoints )
assume A50:
( 1
<= i &
i <= len f2a )
;
f2a /. i is with_endpoints
then A51:
i + 1
<= (len f2a) + 1
by XREAL_1:6;
i <= i + 1
by NAT_1:11;
then A52:
i <= len f2
by A9, A51, XXREAL_0:2;
i in Seg (len f2)
by A50, A52, FINSEQ_1:1;
then A53:
i in dom f2
by FINSEQ_1:def 3;
i in Seg (len f2a)
by A50, FINSEQ_1:1;
then A54:
i in dom f2a
by FINSEQ_1:def 3;
A55:
ex
c3,
c4 being
with_endpoints Curve of
T st
(
c3 = f1 /. i &
c4 = f2 /. i &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A7, A50, A52, A13;
f2 /. i =
f2 . i
by A53, PARTFUN1:def 6
.=
f2a . i
by A54, A8, FINSEQ_1:def 7
.=
f2a /. i
by A54, PARTFUN1:def 6
;
hence
f2a /. i is
with_endpoints
by A55;
verum
end; then consider c2a being
with_endpoints Curve of
T such that A56:
(
Sum f2a = c2a &
dom c2a = [.(inf (dom (f2a /. 1))),(sup (dom (f2a /. (len f2a)))).] &
the_first_point_of c2a = (f2a /. 1) . (inf (dom (f2a /. 1))) &
the_last_point_of c2a = (f2a /. (len f2a)) . (sup (dom (f2a /. (len f2a)))) )
by A6, A7, A9, A22, A40, Th43;
for
i being
Nat st 1
<= i &
i <= len f1a holds
ex
c3,
c4 being
with_endpoints Curve of
T st
(
c3 = f1a /. i &
c4 = f2a /. i &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
proof
let i be
Nat;
( 1 <= i & i <= len f1a implies ex c3, c4 being with_endpoints Curve of T st
( c3 = f1a /. i & c4 = f2a /. i & c3,c4 are_homotopic & dom c3 = dom c4 ) )
assume A57:
( 1
<= i &
i <= len f1a )
;
ex c3, c4 being with_endpoints Curve of T st
( c3 = f1a /. i & c4 = f2a /. i & c3,c4 are_homotopic & dom c3 = dom c4 )
then A58:
i + 1
<= (len f1a) + 1
by XREAL_1:6;
i <= i + 1
by NAT_1:11;
then A59:
i <= len f1
by A6, A58, XXREAL_0:2;
i in Seg (len f1)
by A57, A59, FINSEQ_1:1;
then A60:
i in dom f1
by FINSEQ_1:def 3;
i in Seg (len f1a)
by A57, FINSEQ_1:1;
then A61:
i in dom f1a
by FINSEQ_1:def 3;
i in Seg (len f2)
by A57, A59, A7, FINSEQ_1:1;
then A62:
i in dom f2
by FINSEQ_1:def 3;
i in Seg (len f2a)
by A57, A6, A7, A9, FINSEQ_1:1;
then A63:
i in dom f2a
by FINSEQ_1:def 3;
consider c3,
c4 being
with_endpoints Curve of
T such that A64:
(
c3 = f1 /. i &
c4 = f2 /. i &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A57, A59, A13;
take
c3
;
ex c4 being with_endpoints Curve of T st
( c3 = f1a /. i & c4 = f2a /. i & c3,c4 are_homotopic & dom c3 = dom c4 )
take
c4
;
( c3 = f1a /. i & c4 = f2a /. i & c3,c4 are_homotopic & dom c3 = dom c4 )
A65:
f1 /. i =
f1 . i
by A60, PARTFUN1:def 6
.=
f1a . i
by A61, A5, FINSEQ_1:def 7
.=
f1a /. i
by A61, PARTFUN1:def 6
;
f2 /. i =
f2 . i
by A62, PARTFUN1:def 6
.=
f2a . i
by A63, A8, FINSEQ_1:def 7
.=
f2a /. i
by A63, PARTFUN1:def 6
;
hence
(
c3 = f1a /. i &
c4 = f2a /. i &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A64, A65;
verum
end; then A66:
c1a,
c2a are_homotopic
by A3, A4, A23, A6, A22, A40, A7, A9, A39, A56;
A67:
c1 = c1a + c1b
by A10, A5, A39, Th41;
A68:
c2 = c2a + c2b
by A10, A8, A56, Th41;
A69:
f1 /. (len f1) = c1b
by A5, A6, A17, FINSEQ_1:42;
A70:
0 + 1
< (len f1a) + 1
by A22, XREAL_1:6;
then A71:
( 1
<= len f1a &
len f1a < len f1 )
by A6, NAT_1:13;
then
len f1a in Seg (len f1)
by FINSEQ_1:1;
then A72:
len f1a in dom f1
by FINSEQ_1:def 3;
len f1a in Seg (len f1a)
by A71, FINSEQ_1:1;
then A73:
len f1a in dom f1a
by FINSEQ_1:def 3;
then A74:
f1a /. (len f1a) =
f1a . (len f1a)
by PARTFUN1:def 6
.=
f1 . (len f1a)
by A5, A73, FINSEQ_1:def 7
.=
f1 /. (len f1a)
by A72, PARTFUN1:def 6
;
len f2a in Seg (len f2)
by A71, A6, A9, A7, FINSEQ_1:1;
then A75:
len f2a in dom f2
by FINSEQ_1:def 3;
len f2a in Seg (len f2a)
by A71, A6, A7, A9, FINSEQ_1:1;
then A76:
len f2a in dom f2a
by FINSEQ_1:def 3;
then A77:
f2a /. (len f2a) =
f2a . (len f2a)
by PARTFUN1:def 6
.=
f2 . (len f2a)
by A8, A76, FINSEQ_1:def 7
.=
f2 /. (len f2a)
by A75, PARTFUN1:def 6
;
1
in Seg (len f1)
by A70, A6, FINSEQ_1:1;
then A78:
1
in dom f1
by FINSEQ_1:def 3;
1
in Seg (len f1a)
by A71, FINSEQ_1:1;
then A79:
1
in dom f1a
by FINSEQ_1:def 3;
then A80:
f1a /. 1 =
f1a . 1
by PARTFUN1:def 6
.=
f1 . 1
by A5, A79, FINSEQ_1:def 7
.=
f1 /. 1
by A78, PARTFUN1:def 6
;
1
in Seg (len f2)
by A70, A7, A6, FINSEQ_1:1;
then A81:
1
in dom f2
by FINSEQ_1:def 3;
1
in Seg (len f2a)
by A71, A6, A7, A9, FINSEQ_1:1;
then A82:
1
in dom f2a
by FINSEQ_1:def 3;
then A83:
f2a /. 1 =
f2a . 1
by PARTFUN1:def 6
.=
f2 . 1
by A8, A82, FINSEQ_1:def 7
.=
f2 /. 1
by A81, PARTFUN1:def 6
;
A84:
ex
c3,
c4 being
with_endpoints Curve of
T st
(
c3 = f1 /. 1 &
c4 = f2 /. 1 &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A13, A15;
A85:
ex
c3,
c4 being
with_endpoints Curve of
T st
(
c3 = f1 /. (len f1a) &
c4 = f2 /. (len f1a) &
c3,
c4 are_homotopic &
dom c3 = dom c4 )
by A71, A13;
A86:
the_last_point_of c1a = the_first_point_of c1b
by A69, A6, A74, A11, A71, A39;
sup (dom c1a) =
sup (dom (f1 /. (len f1a)))
by A74, A39, XXREAL_1:29, XXREAL_2:29
.=
inf (dom (f1 /. ((len f1a) + 1)))
by A11, A71
.=
inf (dom c1b)
by A5, A6, A17, FINSEQ_1:42
;
hence
c1,
c2 are_homotopic
by A66, A67, A68, A18, A21, A86, Th39, A56, A84, A85, A80, A83, A6, A7, A9, A74, A77, A39;
verum end; suppose A87:
not
len f1a > 0
;
c1,c2 are_homotopic then
f1a = {}
;
then
f1 = <*c1b*>
by A5, FINSEQ_1:34;
then A88:
Sum f1 = c1b
by Th40;
f2a = {}
by A87, A6, A7, A9;
then
f2 = <*c2b*>
by A8, FINSEQ_1:34;
hence
c1,
c2 are_homotopic
by A88, A18, A21, A10, Th40;
verum end; end;
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A1, A2);
hence
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
; verum