let T be non empty TopSpace; :: thesis:
defpred S₁[ Nat] means for f being FinSequence of Curves T st len f = $1 & 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)))) );
A1: S₁[ 0 ] ;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A3: S₁[k] ; :: thesis:
let f be FinSequence of Curves T; :: thesis:
assume A4: ( len f = k + 1 & len f > 0 ) ; :: thesis:
consider f1 being FinSequence of Curves T, c2 being Element of Curves T such that
A5: f = f1 ^ <*c2*> by A4, FINSEQ_2:19;
A6: len f = (len f1) + (len <*c2*>) by A5, FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:39 ;
assume A7: 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))) ) ; :: thesis:
assume A8: for i being Nat st 1 <= i & i <= len f holds
f /. i is with_endpoints ; :: thesis:
A9: 1 <= len f by A4, NAT_1:12;
len f in Seg (len f) by A4, FINSEQ_1:3;
then A10: len f in dom f by FINSEQ_1:def 3;
c2 = f . (len f) by A5, A6, FINSEQ_1:42
.= f /. (len f) by A10, PARTFUN1:def 6 ;
then reconsider c2 = c2 as with_endpoints Curve of T by A9, A8;
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))) )

proof

let i be Nat; :: thesis:
assume A12: ( 1 <= i & i < len f1 ) ; :: thesis:
A13: i < len f by A6, A12, NAT_1:13;
i in Seg (len f1) by A12, FINSEQ_1:1;
then A14: i in dom f1 by FINSEQ_1:def 3;
A15: dom f1 c= dom f by A5, FINSEQ_1:26;
A16: f /. i = f . i by A15, A14, PARTFUN1:def 6
.= f1 . i by A5, A14, FINSEQ_1:def 7
.= f1 /. i by A14, PARTFUN1:def 6 ;
1 + 1 <= i + 1 by A12, XREAL_1:6;
then A17: 1 <= i + 1 by XXREAL_0:2;
i + 1 <= len f1 by A12, NAT_1:13;
then i + 1 in Seg (len f1) by A17, FINSEQ_1:1;
then A18: i + 1 in dom f1 by FINSEQ_1:def 3;
A19: f /. (i + 1) = f . (i + 1) by A18, A15, PARTFUN1:def 6
.= f1 . (i + 1) by A5, A18, FINSEQ_1:def 7
.= f1 /. (i + 1) by A18, PARTFUN1:def 6 ;
thus ( (f1 /. i) . (sup (dom (f1 /. i))) = (f1 /. (i + 1)) . (inf (dom (f1 /. (i + 1)))) & sup (dom (f1 /. i)) = inf (dom (f1 /. (i + 1))) ) by A16, A19, A13, A12, A7; :: thesis:

end;

A20: for i being Nat st 1 <= i & i <= len f1 holds
f1 /. i is with_endpoints

proof

let i be Nat; :: thesis:
assume A21: ( 1 <= i & i <= len f1 ) ; :: thesis:
A22: i <= len f by A6, A21, NAT_1:13;
i in Seg (len f1) by A21, FINSEQ_1:1;
then A23: i in dom f1 by FINSEQ_1:def 3;
A24: dom f1 c= dom f by A5, FINSEQ_1:26;
f /. i = f . i by A24, A23, PARTFUN1:def 6
.= f1 . i by A5, A23, FINSEQ_1:def 7
.= f1 /. i by A23, PARTFUN1:def 6 ;
hence f1 /. i is with_endpoints by A22, A21, A8; :: thesis:

end;

per cases ;

suppose len f1 = 0 ; :: thesis:

then f1 = {} ;
then A25: f = <*c2*> by A5, FINSEQ_1:34;
take c2 ; :: thesis:
1 in Seg 1 by FINSEQ_1:3;
then A26: 1 in dom f by A25, FINSEQ_1:38;
A27: f /. 1 = f . 1 by A26, PARTFUN1:def 6
.= c2 by A25 ;
A28: f /. (len f) = c2 by A27, A25, FINSEQ_1:40;
thus ( Sum f = c2 & dom c2 = [.(inf (dom (f /. 1))),(sup (dom (f /. (len f)))).] & the_first_point_of c2 = (f /. 1) . (inf (dom (f /. 1))) & the_last_point_of c2 = (f /. (len f)) . (sup (dom (f /. (len f)))) ) by A25, Th40, A27, A28, Th27; :: thesis:

end;

suppose A29: not len f1 = 0 ; :: thesis:

consider c1 being with_endpoints Curve of T such that
A30: ( Sum f1 = c1 & dom c1 = [.(inf (dom (f1 /. 1))),(sup (dom (f1 /. (len f1)))).] & the_first_point_of c1 = (f1 /. 1) . (inf (dom (f1 /. 1))) & the_last_point_of c1 = (f1 /. (len f1)) . (sup (dom (f1 /. (len f1)))) ) by A4, A6, A11, A20, A3, A29;
set c = c1 + c2;
A31: 0 + 1 < (len f1) + 1 by A29, XREAL_1:6;
then A32: 1 <= len f1 by NAT_1:13;
A33: len f1 < len f by A6, NAT_1:13;
then A34: ( (f /. (len f1)) . (sup (dom (f /. (len f1)))) = (f /. ((len f1) + 1)) . (inf (dom (f /. ((len f1) + 1)))) & sup (dom (f /. (len f1))) = inf (dom (f /. ((len f1) + 1))) ) by A32, A7;
(len f1) + 1 in Seg (len f) by A6, A31, FINSEQ_1:1;
then A35: (len f1) + 1 in dom f by FINSEQ_1:def 3;
A36: f /. ((len f1) + 1) = f . ((len f1) + 1) by A35, PARTFUN1:def 6
.= c2 by A5, FINSEQ_1:42 ;
A37: inf (dom (f1 /. 1)) <= sup (dom (f1 /. (len f1))) by A30, XXREAL_1:29;
A38: dom f1 c= dom f by A5, FINSEQ_1:26;
len f1 in Seg (len f1) by A29, FINSEQ_1:3;
then A39: len f1 in dom f1 by FINSEQ_1:def 3;
A40: f1 /. (len f1) = f1 . (len f1) by A39, PARTFUN1:def 6
.= f . (len f1) by A5, A39, FINSEQ_1:def 7
.= f /. (len f1) by A39, A38, PARTFUN1:def 6 ;
A41: sup (dom c1) = inf (dom c2) by A36, A34, A40, A30, XXREAL_1:29, XXREAL_2:29;
A42: the_last_point_of c1 = the_first_point_of c2 by A36, A30, A40, A33, A32, A7;
A43: ( 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 ) by A41, A42, Th38;
1 in Seg (len f1) by A32, FINSEQ_1:1;
then A44: 1 in dom f1 by FINSEQ_1:def 3;
A45: f1 /. 1 = f1 . 1 by A44, PARTFUN1:def 6
.= f . 1 by A44, A5, FINSEQ_1:def 7
.= f /. 1 by A44, A38, PARTFUN1:def 6 ;
reconsider c = c1 + c2 as with_endpoints Curve of T by A41, A42, Th38;
take c ; :: thesis:
inf (dom c1) <= sup (dom c2) by A43, XXREAL_1:29;
hence ( 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)))) ) by A43, A45, A37, A30, A5, Th41, A36, A6, XXREAL_2:25, XXREAL_2:29; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence 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)))) ) ; :: thesis: