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