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 reconsider fj = f . j as Function by FUNCT_6:19;
A4: j in dom f by A3, FUNCT_6:19;
then {} = dom fj by A2, FUNCT_6:22;
then f . j = {} by RELAT_1:41;
hence contradiction by A4, FUNCT_1:def 9; :: thesis: verum

end;

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