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 A24: v1 = f . (len F) and
A25: f . 0 = 0. V and
A26: 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 f' being Function of NAT ,the carrier of V such that A27: v2 = f' . (len F) and
A28: f' . 0 = 0. V and
A29: 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: v1 = v2
defpred S₁[ Element of NAT ] means ( $1 <= len F implies f . $1 = f' . $1 );
A30: S₁[ 0 ] by A25, A28;
A31: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

now

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

end;

hence for k being Element of NAT st S₁[k] holds
S₁[k + 1] ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A30, A31);
hence v1 = v2 by A24, A27; :: thesis: verum