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