let T be non empty TopSpace; :: thesis:
defpred S₁[ 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: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
let f1, f2 be FinSequence of Curves T; :: thesis:
let c1, c2 be with_endpoints Curve of T; :: thesis:
assume A4: ( len f1 = k + 1 & len f1 > 0 ) ; :: thesis:
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 ; :: thesis:
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 ) ; :: thesis:
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))) ) ; :: thesis:
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))) ) ; :: thesis:
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 ) ; :: thesis:
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;

suppose A22: len f1a > 0 ; :: thesis:

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; :: thesis:
assume A24: ( 1 <= i & i < len f1a ) ; :: thesis:
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; :: thesis:

end;

for i being Nat st 1 <= i & i <= len f1a holds
f1a /. i is with_endpoints

proof

let i be Nat; :: thesis:
assume A33: ( 1 <= i & i <= len f1a ) ; :: thesis:
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; :: thesis:

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; :: thesis:
assume A41: ( 1 <= i & i < len f2a ) ; :: thesis:
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; :: thesis:

end;

for i being Nat st 1 <= i & i <= len f2a holds
f2a /. i is with_endpoints

proof

let i be Nat; :: thesis:
assume A50: ( 1 <= i & i <= len f2a ) ; :: thesis:
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; :: thesis:

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; :: thesis:
assume A57: ( 1 <= i & i <= len f1a ) ; :: thesis:
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 ; :: thesis:
take c4 ; :: thesis:
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; :: thesis:

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; :: thesis:

end;

suppose A87: not len f1a > 0 ; :: thesis:

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; :: thesis:

end;

for k being Nat holds S₁[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 ; :: thesis: