per cases ( len f > 0 or len f <= 0 ) ;

suppose A1: len f > 0 ; :: thesis: ex b₁ being FinSequence of Curves T st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

reconsider q = <*(f /. 1)*> as FinSequence of Curves T ;
A2: 0 + 1 <= len f by A1, NAT_1:13;
then f /. 1 = f . 1 by FINSEQ_4:15;
then A3: q . 1 = f . 1 ;
defpred S₁[ Nat] means ( $1 + 1 <= len f implies ex g being FinSequence of Curves T st
( $1 + 1 = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < $1 + 1 holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) ) );
A4: for i being Nat st 1 <= i & i < 0 + 1 holds
q . (i + 1) = (q /. i) + (f /. (i + 1)) ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( ( (k + 1) + 1 <= len f & S₁[k + 1] ) or ( (k + 1) + 1 > len f & S₁[k + 1] ) )

per cases ( (k + 1) + 1 <= len f or (k + 1) + 1 > len f ) ;

case A7: (k + 1) + 1 <= len f ; :: thesis: S₁[k + 1]

k + 1 < (k + 1) + 1 by XREAL_1:29;
then consider g being FinSequence of Curves T such that
A8: k + 1 = len g and
A9: f . 1 = g . 1 and
A10: for i being Nat st 1 <= i & i < k + 1 holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) by A6, A7, XXREAL_0:2;
reconsider g2 = g ^ <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*> as FinSequence of Curves T ;
A11: Seg (len g) = dom g by FINSEQ_1:def 3;
A12: len g2 = (len g) + (len <*((g /. (k + 1)) + (f /. ((k + 1) + 1)))*>) by FINSEQ_1:22
.= (k + 1) + 1 by A8, FINSEQ_1:40 ;
A13: for i being Nat st 1 <= i & i < (k + 1) + 1 holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

proof

let i be Nat; :: thesis: ( 1 <= i & i < (k + 1) + 1 implies g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) )
assume that
A14: 1 <= i and
A15: i < (k + 1) + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))
A16: i <= k + 1 by A15, NAT_1:13;

per cases ( i < k + 1 or i = k + 1 ) by A16, XXREAL_0:1;

suppose A17: i < k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

A18: 1 <= i + 1 by NAT_1:12;
i + 1 <= k + 1 by A17, NAT_1:13;
then i + 1 in Seg (len g) by A8, A18, FINSEQ_1:1;
then A19: g2 . (i + 1) = g . (i + 1) by A11, FINSEQ_1:def 7;
i in Seg (len g) by A8, A14, A16, FINSEQ_1:1;
then A20: g2 . i = g . i by A11, FINSEQ_1:def 7;
A21: g /. i = g . i by A8, A14, A17, FINSEQ_4:15;
g2 /. i = g2 . i by A12, A14, A15, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A10, A14, A17, A19, A20, A21; :: thesis: verum

end;

suppose A22: i = k + 1 ; :: thesis: g2 . (i + 1) = (g2 /. i) + (f /. (i + 1))

A23: g2 /. i = g2 . i by A12, A14, A15, FINSEQ_4:15;
i in Seg (len g) by A8, A14, A16, FINSEQ_1:1;
then A24: g . i = g2 . i by A11, FINSEQ_1:def 7;
g /. i = g . i by A8, A14, A16, FINSEQ_4:15;
hence g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) by A8, A22, A24, A23, FINSEQ_1:42; :: thesis: verum

end;

end;

end;

1 <= k + 1 by NAT_1:11;
then 1 in Seg (len g) by A8, FINSEQ_1:1;
then g2 . 1 = f . 1 by A9, A11, FINSEQ_1:def 7;
hence S₁[k + 1] by A12, A13; :: thesis: verum

end;

case (k + 1) + 1 > len f ; :: thesis: S₁[k + 1]

hence S₁[k + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

(len f) -' 1 = (len f) - 1 by A2, XREAL_1:233;
then A25: ((len f) -' 1) + 1 = len f ;
len q = 1 by FINSEQ_1:40;
then A26: S₁[ 0 ] by A3, A4;
for k being Nat holds S₁[k] from NAT_1:sch 2(A26, A5);
hence ex b₁ being FinSequence of Curves T st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) ) by A25; :: thesis: verum

end;

suppose A27: len f <= 0 ; :: thesis: ex b₁ being FinSequence of Curves T st
( len f = len b₁ & f . 1 = b₁ . 1 & ( for i being Nat st 1 <= i & i < len f holds
b₁ . (i + 1) = (b₁ /. i) + (f /. (i + 1)) ) )

take f ; :: thesis: ( len f = len f & f . 1 = f . 1 & ( for i being Nat st 1 <= i & i < len f holds
f . (i + 1) = (f /. i) + (f /. (i + 1)) ) )
thus ( len f = len f & f . 1 = f . 1 ) ; :: thesis: for i being Nat st 1 <= i & i < len f holds
f . (i + 1) = (f /. i) + (f /. (i + 1))
let i be Nat; :: thesis: ( 1 <= i & i < len f implies f . (i + 1) = (f /. i) + (f /. (i + 1)) )
thus ( 1 <= i & i < len f implies f . (i + 1) = (f /. i) + (f /. (i + 1)) ) by A27; :: thesis: verum

end;

end;