let Q, X, Y be set ; :: thesis: for f being Function of X,Y st Y <> {} holds
for x being object holds
( x in f " Q iff ( x in X & f . x in Q ) )
let f be Function of X,Y; :: thesis: ( Y <> {} implies for x being object holds
( x in f " Q iff ( x in X & f . x in Q ) ) )
assume Y <> {} ; :: thesis: for x being object holds
( x in f " Q iff ( x in X & f . x in Q ) )
then dom f = X by Def1;
hence for x being object holds
( x in f " Q iff ( x in X & f . x in Q ) ) by FUNCT_1:def 7; :: thesis: verum