let X, Y, P be set ; :: thesis: for f being Function of X,Y st Y <> {} holds
for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P
let f be Function of X,Y; :: thesis: ( Y <> {} implies for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P )
assume Y <> {} ; :: thesis: for y being set st ex x being set st
( x in X & x in P & y = f . x ) holds
y in f .: P
then A1: dom f = X by Def1;
let y be set ; :: thesis: ( ex x being set st
( x in X & x in P & y = f . x ) implies y in f .: P )
given x being set such that A2: ( x in X & x in P & y = f . x ) ; :: thesis: y in f .: P
thus y in f .: P by A1, A2, FUNCT_1:def 6; :: thesis: verum