consider f being sequence of F_Real such that
A1: Sum F = f . (len F) and
A2: f . 0 = 0. F_Real and
A3: for j being Nat
for v being Element of F_Real st j < len F & v = F . (j + 1) holds
f . (j + 1) = (f . j) + v by RLVECT_1:def 12;
defpred S1[ Nat] means ( F <= len F implies f . F is integer );
A4: S1[ 0 ] by A2;
A5: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume that
A6: S1[k] and
A7: k + 1 <= len F ; :: thesis: f . (k + 1) is integer
reconsider v = F . (k + 1) as Element of F_Real by XREAL_0:def 1;
A8: k + 0 < k + 1 by XREAL_1:8;
then k < len F by A7, XXREAL_0:2;
then f . (k + 1) = (f . k) + v by A3;
hence f . (k + 1) is integer by A6, A8, A7, XXREAL_0:2; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A4, A5);
 hence Sum F is integer by A1; :: thesis: verum