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

thus for i being object st i in rng f holds
i in {{}} by A1; :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {{}} c= rng f
set e = the Element of dom f;
let i be object ; :: 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;
f . the Element of dom f is empty by A1;
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 object st i in dom f holds
f . i is empty ; :: according to FUNCT_1:def 8 :: thesis: verum

end;

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

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

end;

end;