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