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