let I be non empty closed_interval Subset of REAL; :: thesis: for D being Division of I
for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
let D be Division of I; :: thesis: for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
let fc be Function of I,REAL; :: thesis: ( fc = chi (I,I) implies ( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) ) )
assume A1: fc = chi (I,I) ; :: thesis: ( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
consider i0 being Nat such that
A2: i0 in dom D and
A3: min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i0 by Th43;
min (rng (upper_volume (fc,D))) = vol (divset (D,i0)) by A1, A2, A3, INTEGRA1:20;
hence 0 <= min (rng (upper_volume (fc,D))) by INTEGRA1:9; :: thesis: ( 0 = min (rng (upper_volume (fc,D))) iff divset (D,1) = [.(D . 1),(D . 1).] )
thus ( 0 = min (rng (upper_volume (fc,D))) iff divset (D,1) = [.(D . 1),(D . 1).] ) :: thesis: verum

proof

hereby :: thesis: ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) )

assume 0 = min (rng (upper_volume (fc,D))) ; :: thesis: divset (D,1) = [.(D . 1),(D . 1).]
then A4: vol (divset (D,i0)) = 0 by A3, A1, A2, INTEGRA1:20;
rng D <> {} ;
then 1 in dom D by FINSEQ_3:32;
then D . 1 in I by INTEGRA1:6;
then D . 1 in [.(lower_bound I),(upper_bound I).] by INTEGRA1:4;
then A5: lower_bound I <= D . 1 by XXREAL_1:1;

now :: thesis: divset (D,1) = [.(D . 1),(D . 1).]

( 1 <= i0 & i0 <= len D ) by A2, FINSEQ_3:25;

per cases then ( i0 = 1 or 1 < i0 ) by XXREAL_0:1;

suppose i0 = 1 ; :: thesis: divset (D,1) = [.(D . 1),(D . 1).]

then divset (D,i0) = [.(lower_bound I),(D . 1).] by COUSIN:50;
then ( lower_bound (divset (D,i0)) = lower_bound I & upper_bound (divset (D,i0)) = D . 1 ) by A5, JORDAN5A:19;
then vol (divset (D,i0)) = (D . 1) - (lower_bound I) by INTEGRA1:def 5;
hence divset (D,1) = [.(D . 1),(D . 1).] by A4, COUSIN:50; :: thesis: verum

end;

suppose A6: 1 < i0 ; :: thesis: divset (D,1) = [.(D . 1),(D . 1).]

A7: now :: thesis: ( i0 in dom D & i0 - 1 in dom D & i0 - 1 < i0 )

thus i0 in dom D by A2; :: thesis: ( i0 - 1 in dom D & i0 - 1 < i0 )
thus i0 - 1 in dom D by A6, A2, CGAMES_1:20; :: thesis: i0 - 1 < i0
i0 - 1 < i0 - 0 by XREAL_1:15;
hence i0 - 1 < i0 ; :: thesis: verum

end;

then A8: D . (i0 - 1) < D . i0 by VALUED_0:def 13;
divset (D,i0) = [.(D . (i0 - 1)),(D . i0).] by A6, A2, COUSIN:50;
then ( lower_bound (divset (D,i0)) = D . (i0 - 1) & upper_bound (divset (D,i0)) = D . i0 ) by A8, JORDAN5A:19;
then vol (divset (D,i0)) = (D . i0) - (D . (i0 - 1)) by INTEGRA1:def 5;
hence divset (D,1) = [.(D . 1),(D . 1).] by A4, A7, VALUED_0:def 13; :: thesis: verum

end;

end;

end;

hence divset (D,1) = [.(D . 1),(D . 1).] ; :: thesis: verum

end;

assume A9: divset (D,1) = [.(D . 1),(D . 1).] ; :: thesis: 0 = min (rng (upper_volume (fc,D)))
A10: vol (divset (D,1)) = (upper_bound (divset (D,1))) - (lower_bound (divset (D,1))) by INTEGRA1:def 5
.= (D . 1) - (lower_bound (divset (D,1))) by A9, JORDAN5A:19
.= (D . 1) - (D . 1) by A9, JORDAN5A:19
.= 0 ;
rng D <> {} ;
then A11: 1 in dom D by FINSEQ_3:32;
then A12: (upper_volume (fc,D)) . 1 = 0 by A1, A10, INTEGRA1:20;
1 in Seg (len D) by A11, FINSEQ_1:def 3;
then 1 in Seg (len (upper_volume (fc,D))) by INTEGRA1:def 6;
then A13: 1 in dom (upper_volume (fc,D)) by FINSEQ_1:def 3;

now :: thesis: for i being Nat st i in dom (upper_volume (fc,D)) holds
0 <= (upper_volume (fc,D)) . i

let i be Nat; :: thesis: ( i in dom (upper_volume (fc,D)) implies 0 <= (upper_volume (fc,D)) . i )
assume i in dom (upper_volume (fc,D)) ; :: thesis: 0 <= (upper_volume (fc,D)) . i
then i in Seg (len (upper_volume (fc,D))) by FINSEQ_1:def 3;
then i in Seg (len D) by INTEGRA1:def 6;
then i in dom D by FINSEQ_1:def 3;
then (upper_volume (fc,D)) . i = vol (divset (D,i)) by A1, INTEGRA1:20;
hence 0 <= (upper_volume (fc,D)) . i by INTEGRA1:9; :: thesis: verum

end;

hence 0 = min (rng (upper_volume (fc,D))) by A13, A12, Th45; :: thesis: verum

end;