let p1, p2 be Element of REAL n; :: thesis: ( ( len f > 0 & ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p1 = g . (len f) ) & ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p2 = g . (len f) ) implies p1 = p2 ) & ( not len f > 0 & p1 = 0* n & p2 = 0* n implies p1 = p2 ) )

hereby :: thesis: ( not len f > 0 & p1 = 0* n & p2 = 0* n implies p1 = p2 )

assume len f > 0 ; :: thesis: ( ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p1 = g . (len f) ) & ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p2 = g . (len f) ) implies p1 = p2 )
then A27: 0 + 1 <= len f by NAT_1:13;
assume ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p1 = g . (len f) ) ; :: thesis: ( ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p2 = g . (len f) ) implies p1 = p2 )
then consider g1 being FinSequence of REAL n such 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)) and
A31: p1 = g1 . (len f) ;
assume ex g being FinSequence of REAL n st
( len f = len g & f . 1 = g . 1 & ( for i being Nat st 1 <= i & i < len f holds
g . (i + 1) = (g /. i) + (f /. (i + 1)) ) & p2 = g . (len f) ) ; :: thesis: p1 = p2
then consider g2 being FinSequence of REAL n such that
A32: len f = len g2 and
A33: f . 1 = g2 . 1 and
A34: for i being Nat st 1 <= i & i < len f holds
g2 . (i + 1) = (g2 /. i) + (f /. (i + 1)) and
A35: p2 = g2 . (len f) ;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies g1 . $1 = g2 . $1 );
A36: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A37: 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
A38: k + 1 <= len f ; :: thesis: g1 . (k + 1) = g2 . (k + 1)
A39: k < k + 1 by XREAL_1:31;
then A40: k < len f by A38, XXREAL_0:2;

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

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

then A42: g2 . (k + 1) = (g2 /. k) + (f /. (k + 1)) by A34, A40;
A43: k <= len g2 by A32, A38, A39, XXREAL_0:2;
A44: g1 /. k = g1 . k by A28, A40, A41, FINSEQ_4:24;
g1 . (k + 1) = (g1 /. k) + (f /. (k + 1)) by A30, A40, A41;
hence g1 . (k + 1) = g2 . (k + 1) by A37, A38, A39, A41, A42, A44, A43, FINSEQ_4:24, 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, A33; :: thesis: verum

end;

end;

end;

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

end;

A45: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A45, A36);
hence p1 = p2 by A27, A31, A35; :: thesis: verum

end;

thus ( not len f > 0 & p1 = 0* n & p2 = 0* n implies p1 = p2 ) ; :: thesis: verum