{} in rng f by RELAT_1:def 9;
then A1: product f = {} by CARD_3:26;

now :: thesis: for x being object st x in dom (ProjMap f) holds
(ProjMap f) . x is empty

let x be object ; :: thesis: ( x in dom (ProjMap f) implies (ProjMap f) . x is empty )
assume x in dom (ProjMap f) ; :: thesis: (ProjMap f) . x is empty
then (ProjMap f) . x = proj (f,x) by Def2;
hence (ProjMap f) . x is empty by A1; :: thesis: verum

end;

hence ProjMap f is empty-yielding by FUNCT_1:def 8; :: thesis: verum