let f be Function; :: thesis: ( f is empty-yielding iff ( f = {} or rng f = {{} } ) )

hereby :: thesis: ( ( f = {} or rng f = {{} } ) implies f is empty-yielding )

assume that
A1: f is empty-yielding and
A2: f <> {} ; :: thesis: rng f = {{} }
thus rng f = {{} } :: thesis: verum

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {{} } c= rng f

let i be set ; :: thesis: ( i in rng f implies i in {{} } )
assume i in rng f ; :: thesis: i in {{} }
then ex e being set st
( e in dom f & f . e = i ) by FUNCT_1:def 5;
then i = {} by A1, FUNCT_1:def 14;
hence i in {{} } by TARSKI:def 1; :: thesis: verum

end;

let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in {{} } or i in rng f )
A3: dom f <> {} by A2, RELAT_1:64;
consider e being Element of dom f;
A4: f . e is empty by A1, A3, FUNCT_1:def 14;
assume i in {{} } ; :: thesis: i in rng f
then i = {} by TARSKI:def 1;
hence i in rng f by A3, A4, FUNCT_1:def 5; :: thesis: verum

end;

end;

assume A5: ( f = {} or rng f = {{} } ) ; :: thesis: f is empty-yielding

per cases ( f = {} or rng f = {{} } ) by A5;

suppose f = {} ; :: thesis: f is empty-yielding

hence for i being set st i in dom f holds
f . i is empty by RELAT_1:60; :: according to FUNCT_1:def 14 :: thesis: verum

end;

suppose A6: rng f = {{} } ; :: thesis: f is empty-yielding

let i be set ; :: according to FUNCT_1:def 14 :: thesis: ( not i in dom f or f . i is empty )
assume i in dom f ; :: thesis: f . i is empty
then f . i in rng f by FUNCT_1:def 5;
hence f . i is empty by A6, TARSKI:def 1; :: thesis: verum

end;

end;