consider f being Function such that

A1: dom f = {(k |-> {})} and

A2: rng f = {{}} by FUNCT_1:5;

dom f c= {{}} *

take f ; :: thesis: ( dom f = {(k |-> {})} & rng f = {{}} )

thus ( dom f = {(k |-> {})} & rng f = {{}} ) by A1, A2; :: thesis: verum

A1: dom f = {(k |-> {})} and

A2: rng f = {{}} by FUNCT_1:5;

dom f c= {{}} *

proof

then reconsider f = f as PartFunc of ({{}} *),{{}} by A2, RELSET_1:4;
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;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

take f ; :: thesis: ( dom f = {(k |-> {})} & rng f = {{}} )

thus ( dom f = {(k |-> {})} & rng f = {{}} ) by A1, A2; :: thesis: verum