defpred S₁[ Nat, Real] means ex r being Element of REAL st
( r in rng (f | (divset (D,$1))) & $2 = r * (vol (divset (D,$1))) );
A1: Seg (len D) = dom D by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg (len D) holds
ex x being Element of REAL st S₁[k,x]

proof

let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of REAL st S₁[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of REAL st S₁[k,x]
then A3: k in dom D by FINSEQ_1:def 3;
dom f = A by FUNCT_2:def 1;
then dom (f | (divset (D,k))) = divset (D,k) by A3, INTEGRA1:8, RELAT_1:62;
then not rng (f | (divset (D,k))) is empty by RELAT_1:42;
then consider r being object such that
A4: r in rng (f | (divset (D,k))) ;
reconsider r = r as Element of REAL by A4;
r * (vol (divset (D,k))) is Element of REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[k,x] by A4; :: thesis: verum

end;

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