let i be Element of NAT ; :: thesis: for A being non empty closed_interval Subset of REAL
for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_above holds
(PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))
let A be non empty closed_interval Subset of REAL; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_above holds
(PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st D1 <= D2 & i in dom D1 & f | A is bounded_above holds
(PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))
let f be Function of A,REAL; :: thesis: ( D1 <= D2 & i in dom D1 & f | A is bounded_above implies (PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i)) )
assume that
A1: D1 <= D2 and
A2: i in dom D1 and
A3: f | A is bounded_above ; :: thesis: (PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i))
A4: len (upper_volume (f,D2)) = len D2 by Def5;
i in Seg (len D1) by A2, FINSEQ_1:def 3;
then i in Seg (len (upper_volume (f,D1))) by Def5;
then i in dom (upper_volume (f,D1)) by FINSEQ_1:def 3;
then A5: (PartSums (upper_volume (f,D1))) . i = Sum ((upper_volume (f,D1)) | i) by Def19;
indx (D2,D1,i) in dom D2 by A1, A2, Def18;
then indx (D2,D1,i) in Seg (len (upper_volume (f,D2))) by A4, FINSEQ_1:def 3;
then A6: indx (D2,D1,i) in dom (upper_volume (f,D2)) by FINSEQ_1:def 3;
i in Seg (len D1) by A2, FINSEQ_1:def 3;
then i is non zero Element of NAT by FINSEQ_1:1;
then (PartSums (upper_volume (f,D1))) . i >= Sum ((upper_volume (f,D2)) | (indx (D2,D1,i))) by A1, A2, A3, A5, Th36;
hence (PartSums (upper_volume (f,D1))) . i >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,i)) by A6, Def19; :: thesis: verum