for j being object st j in dom (doms f) holds
not (doms f) . j is empty

proof

let j be object ; :: thesis: ( j in dom (doms f) implies not (doms f) . j is empty )
assume that
A1: j in dom (doms f) and
A2: (doms f) . j is empty ; :: thesis: contradiction
A3: j in dom f by A1, FUNCT_6:def 2;
reconsider fj = f . j as Function ;
A4: j in dom f by A3;
then {} = dom fj by A2, FUNCT_6:22;
then f . j = {} ;
hence contradiction by A4, FUNCT_1:def 9; :: thesis: verum

end;

hence doms f is non-empty by FUNCT_1:def 9; :: thesis: verum