set f = D --> {};

A1: dom (D --> {}) = D ;

A2: rng (D --> {}) = {{}} by FUNCOP_1:8;

rng (D --> {}) c= D

A1: dom (D --> {}) = D ;

A2: rng (D --> {}) = {{}} by FUNCOP_1:8;

rng (D --> {}) c= D

proof

hence
D --> {} is BinominativeFunction of D
by A1, RELSET_1:4; :: thesis: verum
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;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