defpred S_{1}[ Nat, Real] means $2 = |.(vol ((divset (t,$1)),rho)).|;

A1: Seg (len t) = dom t by FINSEQ_1:def 3;

A2: for k being Nat st k in Seg (len t) holds

ex x being Element of REAL st S_{1}[k,x]

A5: ( dom p = Seg (len t) & ( for k being Nat st k in Seg (len t) holds

S_{1}[k,p . k] ) )
from FINSEQ_1:sch 5(A2);

len p = len t by A5, FINSEQ_1:def 3;

hence ex b_{1} being FinSequence of REAL st

( len b_{1} = len t & ( for k being Nat st k in dom t holds

b_{1} . k = |.(vol ((divset (t,k)),rho)).| ) )
by A5, A1; :: thesis: verum

A1: Seg (len t) = dom t by FINSEQ_1:def 3;

A2: for k being Nat st k in Seg (len t) holds

ex x being Element of REAL st S

proof

consider p being FinSequence of REAL such that
let k be Nat; :: thesis: ( k in Seg (len t) implies ex x being Element of REAL st S_{1}[k,x] )

assume k in Seg (len t) ; :: thesis: ex x being Element of REAL st S_{1}[k,x]

|.(vol ((divset (t,k)),rho)).| is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S_{1}[k,x]
; :: thesis: verum

end;assume k in Seg (len t) ; :: thesis: ex x being Element of REAL st S

|.(vol ((divset (t,k)),rho)).| is Element of REAL by XREAL_0:def 1;

hence ex x being Element of REAL st S

A5: ( dom p = Seg (len t) & ( for k being Nat st k in Seg (len t) holds

S

len p = len t by A5, FINSEQ_1:def 3;

hence ex b

( len b

b