{} in rng f
by RELAT_1:def 9;

then A1: product f = {} by CARD_3:26;

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

hence
ProjMap f is empty-yielding
by FUNCT_1:def 8; :: thesis: verum(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;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