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

proof

reconsider a = {} as Element of {{} } by TARSKI:def 1;
let x be set ; :: 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:11;
take f ; :: thesis: ( dom f = {(k |-> {} )} & rng f = {{} } )
thus ( dom f = {(k |-> {} )} & rng f = {{} } ) by A1, A2; :: thesis: verum