let Y, P be set ; :: thesis: for f being Function of {},Y holds f .: P = {}
let f be Function of {},Y; :: thesis: f .: P = {}
set y = the Element of f .: P;
assume f .: P <> {} ; :: thesis: contradiction
then ex x being set st
( x in dom f & x in P & the Element of f .: P = f . x ) by FUNCT_1:def 6;
hence contradiction ; :: thesis: verum