let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for a being Real
for x being set holds
( x in less_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
for x being set holds
( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) )
let a be Real; :: thesis: for x being set holds
( x in less_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_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 < a ) ;
hence ( x in less_dom (f,a) iff ( x in dom f & ex y being Real st
( y = f . x & y < a ) ) ) by MESFUNC1:def 11; :: thesis: verum