let T be non empty TopStruct ; :: thesis:
defpred S₁[ Nat] means for c being with_endpoints Curve of T
for h being FinSequence of REAL st len h = $1 & 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)).] ) );
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 c be with_endpoints Curve of T; :: thesis:
let h be FinSequence of REAL ; :: thesis:
assume A4: ( len h = k + 1 & len h >= 2 & h . 1 = inf (dom c) & h . (len h) = sup (dom c) & h is increasing ) ; :: thesis:
consider h1 being FinSequence of REAL , r being Element of REAL such that
A5: h = h1 ^ <*r*> by A4, FINSEQ_2:19;
A6: len h = (len h1) + 1 by A5, FINSEQ_2:16;
reconsider r1 = h . k as Real ;
consider c1, c2 being Element of Curves T such that
A7: ( c = c1 + c2 & c1 = c | [.(inf (dom c)),r1.] & c2 = c | [.r1,(sup (dom c)).] ) by Th37;
A8: k < k + 1 by NAT_1:13;
1 <= 1 + k by NAT_1:12;
then 1 in Seg (len h) by A4, FINSEQ_1:1;
then A9: 1 in dom h by FINSEQ_1:def 3;

per cases ;

suppose len h1 < 2 ; :: thesis:

then len h1 < 1 + 1 ;
then A10: len h1 <= 1 by NAT_1:13;

per cases ;

suppose h1 = {} ; :: thesis:

then h = <*r*> by A5, FINSEQ_1:34;
then len h = 1 by FINSEQ_1:40;
hence 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)).] ) ) by A4; :: thesis:

end;

suppose h1 <> {} ; :: thesis:

then len h1 >= 1 by FINSEQ_1:20;
then A11: len h1 = 1 by A10, XXREAL_0:1;
set f = <*c*>;
take <*c*> ; :: thesis:
A12: len <*c*> = 1 by FINSEQ_1:40;
thus len <*c*> = (len h) - 1 by A11, A6, FINSEQ_1:40; :: thesis:
thus c = Sum <*c*> by Th40; :: thesis:
thus for i being Nat st 1 <= i & i <= len <*c*> holds
<*c*> /. i = c | [.(h /. i),(h /. (i + 1)).] :: thesis:

proof

let i be Nat; :: thesis:
assume A13: ( 1 <= i & i <= len <*c*> ) ; :: thesis:
then A14: i = 1 by A12, XXREAL_0:1;
i in Seg (len <*c*>) by A13, FINSEQ_1:1;
then A15: i in dom <*c*> by FINSEQ_1:def 3;
A16: h /. i = inf (dom c) by A4, A14, A9, PARTFUN1:def 6;
len h in Seg (len h) by A6, FINSEQ_1:3;
then len h in dom h by FINSEQ_1:def 3;
then A17: h /. (i + 1) = sup (dom c) by A4, A6, A11, A14, PARTFUN1:def 6;
thus <*c*> /. i = <*c*> . i by A15, PARTFUN1:def 6
.= c | (dom c) by A14
.= c | [.(h /. i),(h /. (i + 1)).] by A16, A17, Th27 ; :: thesis:

end;

suppose A18: len h1 >= 2 ; :: thesis:

then A19: 1 < k by A4, A6, XXREAL_0:2;
then k in Seg (len h) by A4, A8, FINSEQ_1:1;
then A20: k in dom h by FINSEQ_1:def 3;
k + 1 in Seg (len h) by A4, FINSEQ_1:4;
then A21: k + 1 in dom h by FINSEQ_1:def 3;
h . k <= h . (k + 1) by A8, A20, A21, A4, VALUED_0:def 13;
then [.(inf (dom c)),r1.] c= [.(inf (dom c)),(sup (dom c)).] by A4, XXREAL_1:34;
then A22: [.(inf (dom c)),r1.] c= dom c by Th27;
A23: dom c1 = (dom c) /\ [.(inf (dom c)),r1.] by A7, RELAT_1:61
.= [.(inf (dom c)),r1.] by A22, XBOOLE_1:28 ;
A24: inf (dom c) <= r1 by A4, A19, A9, A20, VALUED_0:def 13;
then A25: r1 = sup (dom c1) by A23, XXREAL_2:29;
A26: inf (dom c1) = inf (dom c) by A24, A23, XXREAL_2:25;
then inf (dom c1) in [.(inf (dom c)),r1.] by A24, XXREAL_1:1;
then dom c1 is left_end by A23, XXREAL_2:def 5;
then A27: c1 is with_first_point ;
r1 in [.(inf (dom c)),r1.] by A24, XXREAL_1:1;
then dom c1 is right_end by A25, A23, XXREAL_2:def 6;
then A28: c1 is with_last_point ;
reconsider c1 = c1 as with_endpoints Curve of T by A27, A28;
A29: h1 = h | (dom h1) by A5, FINSEQ_1:21;
1 in Seg k by A19, FINSEQ_1:1;
then A30: 1 in dom h1 by A4, A6, FINSEQ_1:def 3;
k in Seg k by A19, FINSEQ_1:1;
then A31: len h1 in dom h1 by A4, A6, FINSEQ_1:def 3;
A32: h1 . 1 = inf (dom c1) by A4, A26, A29, A30, FUNCT_1:49;
A33: h1 . (len h1) = h . k by A6, A4, A29, A31, FUNCT_1:49
.= sup (dom c1) by A24, A23, XXREAL_2:29 ;
A34: dom h c= REAL by NUMBERS:19;
rng h c= REAL ;
then reconsider h0 = h as PartFunc of REAL,REAL by A34, RELSET_1:4;
A35: h0 | (dom h0) is increasing by A4;
len h1 <= len h by A6, NAT_1:19;
then Seg (len h1) c= Seg (len h) by FINSEQ_1:5;
then Seg (len h1) c= dom h by FINSEQ_1:def 3;
then A36: dom h1 c= dom h by FINSEQ_1:def 3;
A37: h1 is increasing by A29, A35;
consider f1 being FinSequence of Curves T such that
A38: ( len f1 = (len h1) - 1 & c1 = Sum f1 & ( for i being Nat st 1 <= i & i <= len f1 holds
f1 /. i = c1 | [.(h1 /. i),(h1 /. (i + 1)).] ) ) by A3, A4, A6, A18, A32, A33, A37;
set f = f1 ^ <*c2*>;
take f1 ^ <*c2*> ; :: thesis:
A39: len (f1 ^ <*c2*>) = (len f1) + (len <*c2*>) by FINSEQ_1:22
.= (len f1) + 1 by FINSEQ_1:40 ;
thus len (f1 ^ <*c2*>) = (len h) - 1 by A6, A38, A39; :: thesis:
thus c = Sum (f1 ^ <*c2*>) by Th41, A7, A38; :: thesis:
thus for i being Nat st 1 <= i & i <= len (f1 ^ <*c2*>) holds
(f1 ^ <*c2*>) /. i = c | [.(h /. i),(h /. (i + 1)).] :: thesis:

proof

let i be Nat; :: thesis:
assume A40: ( 1 <= i & i <= len (f1 ^ <*c2*>) ) ; :: thesis:
then i in Seg (len (f1 ^ <*c2*>)) by FINSEQ_1:1;
then A41: i in dom (f1 ^ <*c2*>) by FINSEQ_1:def 3;

per cases ;

suppose A42: i = len (f1 ^ <*c2*>) ; :: thesis:

A43: h /. i = r1 by A42, A39, A38, A4, A6, A20, PARTFUN1:def 6;
1 + 1 <= i + 1 by A40, XREAL_1:6;
then 1 < len h by A42, A39, A38, A6, XXREAL_0:2;
then len h in Seg (len h) by FINSEQ_1:1;
then len h in dom h by FINSEQ_1:def 3;
then A44: h /. (i + 1) = sup (dom c) by A4, A42, A39, A38, A6, PARTFUN1:def 6;
thus (f1 ^ <*c2*>) /. i = (f1 ^ <*c2*>) . i by A41, PARTFUN1:def 6
.= c | [.(h /. i),(h /. (i + 1)).] by A43, A44, A7, A42, A39, FINSEQ_1:42 ; :: thesis:

end;

suppose i <> len (f1 ^ <*c2*>) ; :: thesis:

then A45: i < (len f1) + 1 by A39, A40, XXREAL_0:1;
then A46: i <= len f1 by NAT_1:13;
then i in Seg (len f1) by A40, FINSEQ_1:1;
then A47: i in dom f1 by FINSEQ_1:def 3;
i in Seg (len h1) by A38, A40, A39, FINSEQ_1:1;
then A48: i in dom h1 by FINSEQ_1:def 3;
A49: h1 /. i = h1 . i by A48, PARTFUN1:def 6
.= (h | (dom h1)) . i by A5, FINSEQ_1:21
.= h . i by A48, FUNCT_1:49
.= h /. i by A48, A36, PARTFUN1:def 6 ;
A50: i + 1 <= len h1 by A38, A45, NAT_1:13;
1 <= i + 1 by NAT_1:12;
then i + 1 in Seg (len h1) by A50, FINSEQ_1:1;
then A51: i + 1 in dom h1 by FINSEQ_1:def 3;
A52: h1 /. (i + 1) = h1 . (i + 1) by A51, PARTFUN1:def 6
.= (h | (dom h1)) . (i + 1) by A5, FINSEQ_1:21
.= h . (i + 1) by A51, FUNCT_1:49
.= h /. (i + 1) by A51, A36, PARTFUN1:def 6 ;
A53: i + 1 <= (len f1) + 1 by A45, NAT_1:13;
h . (i + 1) <= h . k

proof

per cases ;

suppose i + 1 = k ; :: thesis:

hence h . (i + 1) <= h . k ; :: thesis:

end;

suppose i + 1 <> k ; :: thesis:

then i + 1 < k by A38, A6, A4, A53, XXREAL_0:1;
hence h . (i + 1) <= h . k by A51, A36, A20, A4, VALUED_0:def 13; :: thesis:

end;

then A54: h /. (i + 1) <= r1 by A51, A36, PARTFUN1:def 6;
h . 1 <= h . i

proof

per cases ;

suppose i = 1 ; :: thesis:

hence h . 1 <= h . i ; :: thesis:

end;

suppose i <> 1 ; :: thesis:

then 1 < i by A40, XXREAL_0:1;
hence h . 1 <= h . i by A36, A48, A9, A4, VALUED_0:def 13; :: thesis:

end;

then A55: inf (dom c) <= h /. i by A4, A36, A48, PARTFUN1:def 6;
(f1 ^ <*c2*>) . i = f1 . i by A47, FINSEQ_1:def 7
.= f1 /. i by A47, PARTFUN1:def 6
.= (c | [.(inf (dom c)),r1.]) | [.(h1 /. i),(h1 /. (i + 1)).] by A7, A38, A40, A46
.= c | [.(h1 /. i),(h1 /. (i + 1)).] by A55, A52, A49, A54, RELAT_1:74, XXREAL_1:34 ;
hence (f1 ^ <*c2*>) /. i = c | [.(h /. i),(h /. (i + 1)).] by A41, A52, A49, PARTFUN1:def 6; :: thesis:

end;

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