let X, Y, y be set ; :: thesis: for f being PartFunc of X,Y st y in f .: X holds
ex x being Element of X st
( x in dom f & y = f . x )
let f be PartFunc of X,Y; :: thesis: ( y in f .: X implies ex x being Element of X st
( x in dom f & y = f . x ) )
assume y in f .: X ; :: thesis: ex x being Element of X st
( x in dom f & y = f . x )
then ex x being set st
( x in dom f & x in X & y = f . x ) by FUNCT_1:def 6;
hence ex x being Element of X st
( x in dom f & y = f . x ) ; :: thesis: verum