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

proof

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

end;

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