let g1, g2 be FinSequence of Curves T; :: thesis: ( len f = len g1 & f . 1 = g1 . 1 & ( for i being Nat st 1 <= i & i < len f holds
g1 . (i + 1) = (g1 /. i) + (f /. (i + 1)) ) & len f = len g2 & f . 1 = g2 . 1 & ( for i being Nat st 1 <= i & i < len f holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) ) implies g1 = g2 )
assume that
A28: len f = len g1 and
A29: f . 1 = g1 . 1 and
A30: for i being Nat st 1 <= i & i < len f holds
g1 . (i + 1) = (g1 /. i) + (f /. (i + 1)) ; :: thesis: ( not len f = len g2 or not f . 1 = g2 . 1 or ex i being Nat st
( 1 <= i & i < len f & not g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) ) or g1 = g2 )
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies g1 . $1 = g2 . $1 );
assume that
A31: len f = len g2 and
A32: f . 1 = g2 . 1 and
A33: for i being Nat st 1 <= i & i < len f holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) ; :: thesis: g1 = g2
A34: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A35: S₁[k] ; :: thesis: S₁[k + 1]
( 1 <= k + 1 & k + 1 <= len f implies g1 . (k + 1) = g2 . (k + 1) )

proof

assume that
1 <= k + 1 and
A36: k + 1 <= len f ; :: thesis: g1 . (k + 1) = g2 . (k + 1)
A37: k < k + 1 by XREAL_1:29;
then A38: k < len f by A36, XXREAL_0:2;

per cases ( 1 <= k or 1 > k ) ;

suppose A39: 1 <= k ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

then A40: g2 . (k + 1) = (g2 /. k) + (f /. (k + 1)) by A33, A38;
A41: k <= len g2 by A31, A36, A37, XXREAL_0:2;
A42: g1 /. k = g1 . k by A28, A38, A39, FINSEQ_4:15;
g1 . (k + 1) = (g1 /. k) + (f /. (k + 1)) by A30, A38, A39;
hence g1 . (k + 1) = g2 . (k + 1) by A35, A36, A37, A39, A40, A42, A41, FINSEQ_4:15, XXREAL_0:2; :: thesis: verum

end;

suppose 1 > k ; :: thesis: g1 . (k + 1) = g2 . (k + 1)

then 0 + 1 > k ;
then k = 0 by NAT_1:13;
hence g1 . (k + 1) = g2 . (k + 1) by A29, A32; :: thesis: verum

end;

end;

end;

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

end;

A43: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A43, A34);
hence g1 = g2 by A28, A31, FINSEQ_1:14; :: thesis: verum