let a, b be Element of REAL ; :: thesis: ( ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & a = g . ((len f) -' 1) ) & ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b = g . ((len f) -' 1) ) implies a = b )

now

assume C1: ( ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & a = g . ((len f) -' 1) ) & ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b = g . ((len f) -' 1) ) ) ; :: thesis: a = b
then consider g1 being XFinSequence of REAL such that
C2: ( len f = len g1 & f . 0 = g1 . 0 & ( for i being Nat st i + 1 < len f holds
g1 . (i + 1) = (g1 . i) + (f . (i + 1)) ) & a = g1 . ((len f) -' 1) ) ;
consider g2 being XFinSequence of REAL such that
C3: ( len f = len g2 & f . 0 = g2 . 0 & ( for i being Nat st i + 1 < len f holds
g2 . (i + 1) = (g2 . i) + (f . (i + 1)) ) & b = g2 . ((len f) -' 1) ) by C1;
defpred S₁[ Nat] means ( $1 < len g1 implies g1 . $1 = g2 . $1 );
A31: S₁[ 0 ] by C2, C3;
A32: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B0: S₁[k] ; :: thesis: S₁[k + 1]

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

suppose D1: k + 1 < len g1 ; :: thesis: S₁[k + 1]

D3n: k < k + 1 by XREAL_1:31;
g1 . (k + 1) = g2 . (k + 1)

proof

g1 . (k + 1) = (g1 . k) + (f . (k + 1)) by C2, D1;
hence g1 . (k + 1) = g2 . (k + 1) by D3n, B0, D1, C2, C3, XXREAL_0:2; :: thesis: verum

end;

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

end;

suppose k + 1 >= len g1 ; :: thesis: S₁[k + 1]

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

end;

end;

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A31, A32);
hence a = b by C3, C2, AFINSQ_1:11; :: thesis: verum

end;

hence ( ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & a = g . ((len f) -' 1) ) & ex g being XFinSequence of REAL st
( len f = len g & f . 0 = g . 0 & ( for i being Nat st i + 1 < len f holds
g . (i + 1) = (g . i) + (f . (i + 1)) ) & b = g . ((len f) -' 1) ) implies a = b ) ; :: thesis: verum