consider f being Function such that
A1: dom f = {(k |-> {})} and
A2: rng f = {{}} by FUNCT_1:5;
dom f c= {{}} *

proof

reconsider a = {} as Element of {{}} by TARSKI:def 1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom f or x in {{}} * )
assume x in dom f ; :: thesis: x in {{}} *
then x = k |-> a by A1, TARSKI:def 1;
hence x in {{}} * by FINSEQ_1:def 11; :: thesis: verum

end;

then reconsider f = f as PartFunc of ({{}} *),{{}} by A2, RELSET_1:4;
take f ; :: thesis: ( dom f = {(k |-> {})} & rng f = {{}} )
thus ( dom f = {(k |-> {})} & rng f = {{}} ) by A1, A2; :: thesis: verum