defpred S1[ Nat, Real] means ex r being Real st
( r in rng (u | (divset (t,\$1))) & \$2 = r * (vol ((divset (t,\$1)),rho)) );
A1: Seg (len t) = dom t by FINSEQ_1:def 3;
A2: for k being Nat st k in Seg (len t) holds
ex x being Element of REAL st S1[k,x]
proof
let k be Nat; :: thesis: ( k in Seg (len t) implies ex x being Element of REAL st S1[k,x] )
assume k in Seg (len t) ; :: thesis: ex x being Element of REAL st S1[k,x]
then A3: k in dom t by FINSEQ_1:def 3;
dom (u | (divset (t,k))) = divset (t,k) by ;
then not rng (u | (divset (t,k))) is empty by RELAT_1:42;
then consider r being object such that
A4: r in rng (u | (divset (t,k))) ;
reconsider r = r as Element of REAL by A4;
r * (vol ((divset (t,k)),rho)) is Element of REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S1[k,x] by A4; :: thesis: verum
end;
consider p being FinSequence of REAL such that
A5: ( dom p = Seg (len t) & ( for k being Nat st k in Seg (len t) holds
S1[k,p . k] ) ) from len p = len t by ;
hence ex b1 being FinSequence of REAL st
( len b1 = len t & ( for k being Nat st k in dom t holds
ex r being Real st
( r in rng (u | (divset (t,k))) & b1 . k = r * (vol ((divset (t,k)),rho)) ) ) ) by A5, A1; :: thesis: verum