let D be non empty set ; :: thesis: for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y ex N being increasing sequence of NAT st
for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1
let Y be with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y ex N being increasing sequence of NAT st
for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1
let s be non-empty sequence of Y; :: thesis: ex N being increasing sequence of NAT st
for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1
defpred S₁[ Nat, Nat] means $2 = ((Partial_Sums (Length s)) . $1) - 1;
A1: for k being Element of NAT ex n being Element of NAT st S₁[k,n]

proof

let k be Element of NAT ; :: thesis: ex n being Element of NAT st S₁[k,n]
reconsider n = ((Partial_Sums (Length s)) . k) - 1 as Element of NAT by Th7, NAT_1:20;
take n ; :: thesis: S₁[k,n]
thus S₁[k,n] ; :: thesis: verum

end;

consider N being Function of NAT,NAT such that
A2: for k being Element of NAT holds S₁[k,N . k] from FUNCT_2:sch 3(A1);
A3: for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1

proof

let k be Nat; :: thesis: N . k = ((Partial_Sums (Length s)) . k) - 1
k is Element of NAT by ORDINAL1:def 12;
hence N . k = ((Partial_Sums (Length s)) . k) - 1 by A2; :: thesis: verum

end;

for n being Nat holds N . n < N . (n + 1)

proof

let n be Nat; :: thesis: N . n < N . (n + 1)
((Partial_Sums (Length s)) . n) - 1 < ((Partial_Sums (Length s)) . (n + 1)) - 1 by Th7, XREAL_1:9;
then N . n < ((Partial_Sums (Length s)) . (n + 1)) - 1 by A3;
hence N . n < N . (n + 1) by A3; :: thesis: verum

end;

then reconsider N = N as increasing sequence of NAT by VALUED_1:def 13;
take N ; :: thesis: for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1
thus for k being Nat holds N . k = ((Partial_Sums (Length s)) . k) - 1 by A3; :: thesis: verum