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

proof

let j be set ; :: 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 f " (SubFuncs (rng f)) by A1, FUNCT_6:def 2;
then A4: ( j in dom f & f . j is Function ) by FUNCT_6:28;
reconsider fj = f . j as Function by A3, FUNCT_6:28;
{} = dom fj by A2, A4, FUNCT_6:31;
then f . j = {} by RELAT_1:64;
hence contradiction by A4, FUNCT_1:def 15; :: thesis: verum

end;

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