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_below holds
(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_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_below holds
(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_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_below holds
(PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_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_below implies (PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i)) )
assume that
A1: D1 <= D2 and
A2: i in dom D1 and
A3: f | A is bounded_below ; :: thesis: (PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i))
A4: len (lower_volume (f,D2)) = len D2 by Def6;
i in Seg (len D1) by A2, FINSEQ_1:def 3;
then i in Seg (len (lower_volume (f,D1))) by Def6;
then i in dom (lower_volume (f,D1)) by FINSEQ_1:def 3;
then A5: (PartSums (lower_volume (f,D1))) . i = Sum ((lower_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 (lower_volume (f,D2))) by A4, FINSEQ_1:def 3;
then A6: indx (D2,D1,i) in dom (lower_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 (lower_volume (f,D1))) . i <= Sum ((lower_volume (f,D2)) | (indx (D2,D1,i))) by A1, A2, A3, A5, Th37;
hence (PartSums (lower_volume (f,D1))) . i <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,i)) by A6, Def19; :: thesis: verum