defpred S1[ 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 S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len D) implies ex x being Element of the carrier of X st S1[k,x] )
assume k in Seg (len D) ; :: thesis: ex x being Element of the carrier of X st S1[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 ;
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 S1[k,x] by A4; :: thesis: verum
end;
consider p being FinSequence of the carrier of X such that
A5: ( dom p = Seg (len D) & ( for k being Nat st k in Seg (len D) holds
S1[k,p . k] ) ) from len p = len D by ;
hence ex b1 being FinSequence of X st
( len b1 = 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))) & b1 . i = (vol (divset (D,i))) * c ) ) ) by A5, A1; :: thesis: verum