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;
( 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)
;
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 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
S1[
k,
x]
by A4;
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 FINSEQ_1:sch 5(A2);
len p = len D
by A5, FINSEQ_1:def 3;
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; verum