let y be object ; :: thesis: for X, Y being set
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 X, 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 object 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