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_eq_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_eq_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_eq_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_eq_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 <= f . x ) ;
hence ( x in great_eq_dom (f,r) iff ( x in dom f & ex y being Real st
( y = f . x & r <= y ) ) ) by MESFUNC1:def 14; :: thesis: verum