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

proof

let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of REAL n st S₁[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of REAL n st S₁[k,x]
then A10: 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 A10, 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
A11: r in rng (f | (divset D,k)) by XBOOLE_0:def 1;
reconsider r = r as Element of REAL n by A11;
(vol (divset D,k)) * r is Element of REAL n ;
hence ex x being Element of REAL n st S₁[k,x] by A11; :: thesis: verum

end;

consider p being FinSequence of REAL n such that
B1: ( 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, B1;
hence ex b₁ being FinSequence of REAL n st
( len b₁ = len D & ( for i being Nat st i in dom D holds
ex r being Element of REAL n st
( r in rng (f | (divset D,i)) & b₁ . i = (vol (divset D,i)) * r ) ) ) by B1; :: thesis: verum