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 that
A25: 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) ) and
A26: 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
consider g1 being XFinSequence of REAL such that
A27: len f = len g1 and
A28: f . 0 = g1 . 0 and
A29: for i being Nat st i + 1 < len f holds
g1 . (i + 1) = (g1 . i) + (f . (i + 1)) and
A30: a = g1 . ((len f) -' 1) by A25;
consider g2 being XFinSequence of REAL such that
A31: len f = len g2 and
A32: f . 0 = g2 . 0 and
A33: for i being Nat st i + 1 < len f holds
g2 . (i + 1) = (g2 . i) + (f . (i + 1)) and
A34: b = g2 . ((len f) -' 1) by A26;
defpred S₁[ Nat] means ( $1 < len g1 implies g1 . $1 = g2 . $1 );
A35: 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 A36: S₁[k] ; :: thesis: S₁[k + 1]

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

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

A38: k < k + 1 by XREAL_1:31;
g1 . (k + 1) = (g1 . k) + (f . (k + 1)) by A27, A29, A37;
hence S₁[k + 1] by A27, A33, A36, A38, XXREAL_0:2; :: thesis: verum

end;

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

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

end;

end;

end;

A39: S₁[ 0 ] by A28, A32;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A39, A35);
hence a = b by A27, A30, A31, A34, 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