let v1, v2 be Element of V; :: thesis: ( ex f being Function of NAT, the carrier of V st
( v1 = f . (len F) & f . 0 = 0. V & ( for j being Element of 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 Function of NAT, the carrier of V st
( v2 = f . (len F) & f . 0 = 0. V & ( for j being Element of 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 Function of NAT, the carrier of V such that A26: v1 = f . (len F) and
A27: f . 0 = 0. V and
A28: for j being Element of 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 Function of NAT, the carrier of V holds
( not v2 = f . (len F) or not f . 0 = 0. V or ex j being Element of 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 Function of NAT, the carrier of V such that A29: v2 = f9 . (len F) and
A30: f9 . 0 = 0. V and
A31: for j being Element of 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₁[ Element of NAT ] means ( $1 <= len F implies f . $1 = f9 . $1 );

now

A32: rng F c= the carrier of V by FINSEQ_1:def 4;
let k be Element of NAT ; :: thesis: ( ( k <= len F implies f . k = f9 . k ) & k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A33: ( k <= len F implies f . k = f9 . k ) ; :: thesis: ( k + 1 <= len F implies f . (k + 1) = f9 . (k + 1) )
assume A34: 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 A34, FINSEQ_1:3;
then F . (k + 1) in rng F by FUNCT_1:def 5;
then reconsider u1 = F . (k + 1) as Element of V by A32;
A35: k < len F by A34, NAT_1:13;
then f . (k + 1) = (f . k) + u1 by A28;
hence f . (k + 1) = f9 . (k + 1) by A31, A33, A35; :: thesis: verum

end;

then A36: for k being Element of NAT st S₁[k] holds
S₁[k + 1] ;
A37: S₁[ 0 ] by A27, A30;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A37, A36);
hence v1 = v2 by A26, A29; :: thesis: verum