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