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