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 consider x being set such that
A1: x in dom f and
x in X and
A2: y = f . x by FUNCT_1:def 12;
thus ex x being Element of X st
( x in dom f & y = f . x ) by A1, A2; :: thesis: verum