defpred S₁[ 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₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len t) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (len t) ; :: thesis: ex x being Element of REAL st S₁[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₁[k,x] ; :: thesis: verum

end;

consider p being FinSequence of REAL such that
A5: ( dom p = Seg (len t) & ( for k being Nat st k in Seg (len t) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 5(A2);
len p = len t by A5, FINSEQ_1:def 3;
hence ex b₁ being FinSequence of REAL st
( len b₁ = len t & ( for k being Nat st k in dom t holds
b₁ . k = |.(vol ((divset (t,k)),rho)).| ) ) by A5, A1; :: thesis: verum