defpred S₁[ Nat, Element of REAL ] means ex r being Element of REAL st
( r in rng (f | (divset D,$1)) & $2 = r * (vol (divset D,$1)) );
A1: 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 B1: k in dom D by FINSEQ_1:def 3;
not rng (f | (divset D,k)) is empty

proof

dom f = A by FUNCT_2:def 1;
then dom (f | (divset D,k)) = divset D,k by B1, INTEGRA1:10, RELAT_1:91;
hence not rng (f | (divset D,k)) is empty by RELAT_1:65; :: thesis: verum

end;

then consider r being set such that
B2: r in rng (f | (divset D,k)) by XBOOLE_0:def 1;
reconsider r = r as Element of REAL by B2;
r * (vol (divset D,k)) is Element of REAL ;
hence ex x being Element of REAL st S₁[k,x] by B2; :: thesis: verum

end;

consider p being FinSequence of REAL such that
A2: ( 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(A1);
( len p = len D & Seg (len D) = dom D ) by FINSEQ_1:def 3, A2;
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 A2; :: thesis: verum