let i be Element of NAT ; :: thesis: for A being 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 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: i is non empty Element of NAT

proof

i in Seg (len D1) by A2, FINSEQ_1:def 3;
hence i is non empty Element of NAT by FINSEQ_1:3; :: thesis: verum

end;

indx D2,D1,i in Seg (len (upper_volume f,D2))

proof

A6: len (upper_volume f,D2) = len D2 by Def7;
indx D2,D1,i in dom D2 by A1, A2, Def21;
hence indx D2,D1,i in Seg (len (upper_volume f,D2)) by A6, FINSEQ_1:def 3; :: thesis: verum

end;

then B5: 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 in Seg (len (upper_volume f,D1)) by Def7;
then i in dom (upper_volume f,D1) by FINSEQ_1:def 3;
then (PartSums (upper_volume f,D1)) . i = Sum ((upper_volume f,D1) | i) by Def22;
then (PartSums (upper_volume f,D1)) . i >= Sum ((upper_volume f,D2) | (indx D2,D1,i)) by A1, A2, A3, A4, Th40;
hence (PartSums (upper_volume f,D1)) . i >= (PartSums (upper_volume f,D2)) . (indx D2,D1,i) by Def22, B5; :: thesis: verum