let I be non empty closed_interval Subset of REAL; :: thesis: for f being bounded Function of I,REAL holds
( |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 iff f is constant )
let f be bounded Function of I,REAL; :: thesis: ( |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 iff f is constant )
A1: rng f is real-bounded by INTEGRA1:15;
hereby :: thesis: ( f is constant implies |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 )
assume |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 ; :: thesis: f is constant
then (upper_bound (rng f)) - (lower_bound (rng f)) = 0 ;
then ex r being Real st rng f = {r} by A1, Th10;
hence f is constant ; :: thesis: verum
end;
assume f is constant ; :: thesis: |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0
then consider y being Element of REAL such that
A2: rng f = {y} by FUNCT_2:111;
( upper_bound (rng f) = y & lower_bound (rng f) = y ) by A2, SEQ_4:9;
hence |.((upper_bound (rng f)) - (lower_bound (rng f))).| = 0 ; :: thesis: verum