let C be non empty set ; :: thesis: for a, b being Element of REAL
for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )
let a, b be Element of REAL ; :: thesis: for f being PartFunc of C,REAL st rng f c= [.a,b.] & a <= b holds
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )
let f be PartFunc of C,REAL; :: thesis: ( rng f c= [.a,b.] & a <= b implies for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) )
assume that
A1: rng f c= [.a,b.] and
A2: a <= b ; :: thesis: for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )
for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b )

proof

reconsider A = [.a,b.] as non empty closed_interval Subset of REAL by A2, MEASURE5:14;
let x be Element of C; :: thesis: ( x in dom f implies ( a <= f . x & f . x <= b ) )
A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4;
then A3: ( a = lower_bound A & b = upper_bound A ) by INTEGRA1:5;
assume x in dom f ; :: thesis: ( a <= f . x & f . x <= b )
then f . x in rng f by FUNCT_1:def 3;
hence ( a <= f . x & f . x <= b ) by A1, A3, INTEGRA2:1; :: thesis: verum

end;

hence for x being Element of C st x in dom f holds
( a <= f . x & f . x <= b ) ; :: thesis: verum