let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I
for fc being Function of I,REAL ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )
let D be Division of I; :: thesis: for fc being Function of I,REAL ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )
let fc be Function of I,REAL; :: thesis: ex i being Nat st
( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )
inf (rng (upper_volume (fc,D))) in rng (upper_volume (fc,D)) by XXREAL_2:def 5;
then consider x being object such that
A1: x in dom (upper_volume (fc,D)) and
A2: (upper_volume (fc,D)) . x = inf (rng (upper_volume (fc,D))) by FUNCT_1:def 3;
A3: dom (upper_volume (fc,D)) = Seg (len (upper_volume (fc,D))) by FINSEQ_1:def 3
.= Seg (len D) by INTEGRA1:def 6
.= dom D by FINSEQ_1:def 3 ;
reconsider i = x as Nat by A1;
take i ; :: thesis: ( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i )
thus ( i in dom D & min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i ) by A2, A3, A1; :: thesis: verum