let y be object ; :: thesis: for X, Y being set
for f being PartFunc of X,Y st y in rng f 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 rng f 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 rng f implies ex x being Element of X st
( x in dom f & y = f . x ) )
assume y in rng f ; :: 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 & y = f . x ) by FUNCT_1:def 3;
hence ex x being Element of X st
( x in dom f & y = f . x ) ; :: thesis: verum