defpred S_{1}[ Nat, set ] means ex c being Point of X st

( c in rng (f | (divset (D,$1))) & $2 = (vol (divset (D,$1))) * c );

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 the carrier of X st S_{1}[k,x]

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

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

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

hence ex b_{1} being FinSequence of X st

( len b_{1} = len D & ( for i being Nat st i in dom D holds

ex c being Point of X st

( c in rng (f | (divset (D,i))) & b_{1} . i = (vol (divset (D,i))) * c ) ) )
by A5, A1; :: thesis: verum

( c in rng (f | (divset (D,$1))) & $2 = (vol (divset (D,$1))) * c );

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 the carrier of X st S

proof

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

assume k in Seg (len D) ; :: thesis: ex x being Element of the carrier of X st S_{1}[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 c being object such that

A4: c in rng (f | (divset (D,k))) ;

reconsider c = c as Point of X by A4;

(vol (divset (D,k))) * c is Element of the carrier of X ;

hence ex x being Element of the carrier of X st S_{1}[k,x]
by A4; :: thesis: verum

end;assume k in Seg (len D) ; :: thesis: ex x being Element of the carrier of X st S

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 c being object such that

A4: c in rng (f | (divset (D,k))) ;

reconsider c = c as Point of X by A4;

(vol (divset (D,k))) * c is Element of the carrier of X ;

hence ex x being Element of the carrier of X st S

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

S

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

hence ex b

( len b

ex c being Point of X st

( c in rng (f | (divset (D,i))) & b