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 3;
then i = {} by A1, FUNCT_1:def 8;
hence i in {{}} by TARSKI:def 1; :: thesis: verum

end;

set e = the Element of dom f;
let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in {{}} or i in rng f )
assume i in {{}} ; :: thesis: i in rng f
then A3: i = {} by TARSKI:def 1;
A4: dom f <> {} by A2, RELAT_1:41;
then f . the Element of dom f is empty by A1, FUNCT_1:def 8;
hence i in rng f by A4, A3, FUNCT_1:def 3; :: 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:38; :: according to FUNCT_1:def 8 :: thesis: verum

end;

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

let i be set ; :: according to FUNCT_1:def 8 :: thesis: ( not i in proj1 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 3;
hence f . i is empty by A6, TARSKI:def 1; :: thesis: verum

end;

end;