hereby :: thesis: ( ( for n being set st n in dom F holds
not F . n is empty ) implies F is non-empty )

assume F is non-empty ; :: thesis: for i being set st i in dom F holds
not F . i is empty
then A1: not {} in rng F by RELAT_1:def 9;
let i be set ; :: thesis: ( i in dom F implies not F . i is empty )
assume i in dom F ; :: thesis: not F . i is empty
hence not F . i is empty by A1, Def5; :: thesis: verum

end;

assume A2: for n being set st n in dom F holds
not F . n is empty ; :: thesis: F is non-empty
assume {} in rng F ; :: according to RELAT_1:def 9 :: thesis: contradiction
then ex i being set st
( i in dom F & F . i = {} ) by Def5;
hence contradiction by A2; :: thesis: verum