let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for a being real number
for x being set holds
( x in less_eq_dom f,a iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let f be PartFunc of X,REAL ; :: thesis: for a being real number
for x being set holds
( x in less_eq_dom f,a iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let a be real number ; :: thesis: for x being set holds
( x in less_eq_dom f,a iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
let x be set ; :: thesis: ( x in less_eq_dom f,a iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) )
( ex y being Real st
( y = f . x & y <= a ) iff f . x <= R_EAL a ) ;
hence ( x in less_eq_dom f,a iff ( x in dom f & ex y being Real st
( y = f . x & y <= a ) ) ) by MESFUNC1:def 13; :: thesis: verum