let v1, v2 be Element of V; :: thesis: ( ex f being sequence of V st
( v1 = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) & ex f being sequence of V st
( v2 = f . (len F) & f . 0 = 0. V & ( for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ) ) implies v1 = v2 )
given f being sequence of V such that A27: v1 = f . (len F) and
A28: f . 0 = 0. V and
A29: for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v ; :: thesis: ( for f being sequence of V holds
( not v2 = f . (len F) or not f . 0 = 0. V or ex j being Nat ex v being Element of V st
( j < len F & v = F . (j + 1) & not f . (j + 1) = (f . j) + v ) ) or v1 = v2 )
given f9 being sequence of V such that A30: v2 = f9 . (len F) and
A31: f9 . 0 = 0. V and
A32: for j being Nat
for v being Element of V st j < len F & v = F . (j + 1) holds
f9 . (j + 1) = (f9 . j) + v ; :: thesis: v1 = v2
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 = f9 . $1 );

now :: thesis: for k being Nat st ( k <= len F implies f . k = f9 . k ) & k + 1 <= len F holds
f . (k + 1) = f9 . (k + 1)

A33: rng F c= the carrier of V by RELAT_1:def 19;
let k be Nat; :: thesis: ( ( k <= len F implies f . k = f9 . k ) & k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A34: ( k <= len F implies f . k = f9 . k ) ; :: thesis: ( k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A35: k + 1 <= len F ; :: thesis: f . (k + 1) = f9 . (k + 1)
( 1 <= k + 1 & dom F = Seg (len F) ) by FINSEQ_1:def 3, NAT_1:11;
then k + 1 in dom F by A35, FINSEQ_1:1;
then F . (k + 1) in rng F by FUNCT_1:def 3;
then reconsider u1 = F . (k + 1) as Element of V by A33;
A36: k < len F by A35, NAT_1:13;
then f . (k + 1) = (f . k) + u1 by A29;
hence f . (k + 1) = f9 . (k + 1) by A32, A34, A36; :: thesis: verum

end;

then A37: for k being Nat st S₁[k] holds
S₁[k + 1] ;
A38: S₁[ 0 ] by A28, A31;
for k being Nat holds S₁[k] from NAT_1:sch 2(A38, A37);
hence v1 = v2 by A27, A30; :: thesis: verum