let v1, v2 be Element of V; :: thesis:
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:
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:
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 = f9 . $1 );

A33: rng F c= the carrier of V by RELAT_1:def 19;
let k be Nat; :: thesis:
assume A34: ( k <= len F implies f . k = f9 . k ) ; :: thesis:
assume A35: k + 1 <= len F ; :: thesis:
( 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:

end;