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 )

( a <= f . x & f . x <= b ) ; :: thesis: verum

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

hence
for x being Element of C st x in dom f holds
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;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

( a <= f . x & f . x <= b ) ; :: thesis: verum