for j being object st j in dom (doms f) holds

not (doms f) . j is empty

not (doms f) . j is empty

proof

hence
doms f is non-empty
by FUNCT_1:def 9; :: thesis: verum
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;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