let A be non empty closed_interval Subset of REAL; :: thesis: for D being Division of A
for q being FinSequence of REAL st dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) holds
Sum q = vol A
let D be Division of A; :: thesis: for q being FinSequence of REAL st dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) holds
Sum q = vol A
let q be FinSequence of REAL ; :: thesis: ( dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) implies Sum q = vol A )
assume A1: ( dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) ) ; :: thesis: Sum q = vol A
set p = lower_volume ((chi (A,A)),D);
dom q = Seg (len D) by A1
.= Seg (len (lower_volume ((chi (A,A)),D))) by INTEGRA1:def 7 ;
then A2: dom q = dom (lower_volume ((chi (A,A)),D)) by FINSEQ_1:def 3;
for k being Nat st k in dom q holds
q . k = (lower_volume ((chi (A,A)),D)) . k

proof

let k be Nat; :: thesis: ( k in dom q implies q . k = (lower_volume ((chi (A,A)),D)) . k )
assume A3: k in dom q ; :: thesis: q . k = (lower_volume ((chi (A,A)),D)) . k
then A4: q . k = vol (divset (D,k)) by A1;
k in dom D by A3, A1, FINSEQ_1:def 3;
hence q . k = (lower_volume ((chi (A,A)),D)) . k by A4, INTEGRA1:19; :: thesis: verum

end;

then q = lower_volume ((chi (A,A)),D) by A2, FINSEQ_1:13;
hence Sum q = vol A by INTEGRA1:23; :: thesis: verum