set f = D --> {};
A1: dom (D --> {}) = D ;
A2: rng (D --> {}) = {{}} by FUNCOP_1:8;
rng (D --> {}) c= D

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (D --> {}) or x in D )
assume x in rng (D --> {}) ; :: thesis: x in D
then x = {} by A2, TARSKI:def 1;
hence x in D by SETFAM_1:def 8; :: thesis: verum

end;

hence D --> {} is BinominativeFunction of D by A1, RELSET_1:4; :: thesis: verum