assume {} in rng f ; :: according to SETFAM_1:def 8 :: thesis: contradiction
then ex x being object st
( x in dom f & {} = f . x ) by Def3;
hence contradiction by Def9; :: thesis: verum