hereby :: thesis: ( ( for x being object st x in dom f holds
f . x is empty ) implies f is empty-yielding )

assume A1: f is empty-yielding ; :: thesis: for x being object st x in dom f holds
f . x is empty
let x be object ; :: thesis: ( x in dom f implies f . x is empty )
assume x in dom f ; :: thesis: f . x is empty
then f . x in rng f by Def3;
hence f . x is empty by A1, RELAT_1:149; :: thesis: verum

end;

assume A2: for x being object st x in dom f holds
f . x is empty ; :: thesis: f is empty-yielding
let s be object ; :: according to TARSKI:def 3,RELAT_1:def 15 :: thesis: ( not s in rng f or s in {{}} )
assume s in rng f ; :: thesis: s in {{}}
then ex e being object st
( e in dom f & s = f . e ) by Def3;
then s = {} by A2;
hence s in {{}} by TARSKI:def 1; :: thesis: verum