let f be Function; :: thesis: ( product f = {} iff {} in rng f )
thus ( product f = {} implies {} in rng f ) :: thesis: ( {} in rng f implies product f = {} )

proof

assume A1: ( product f = {} & not {} in rng f ) ; :: thesis: contradiction

A2: now

assume dom f = {} ; :: thesis: contradiction
then for x being set st x in dom f holds
f . x in f . x ;
hence contradiction by A1, Def5; :: thesis: verum

end;

now

assume dom f <> {} ; :: thesis: contradiction
then reconsider M = rng f as non empty set by RELAT_1:65;
for X being set st X in M holds
X <> {} by A1;
then consider f1 being Function such that
A3: ( dom f1 = M & ( for X being set st X in M holds
f1 . X in X ) ) by WELLORD2:28;
deffunc H₁( set ) -> set = f1 . (f . $1);
consider g being Function such that
A4: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = H₁(x) ) ) from FUNCT_1:sch 3();

now

let x be set ; :: thesis: ( x in dom f implies g . x in f . x )
assume x in dom f ; :: thesis: g . x in f . x
then ( f . x in M & f . x = f . x & g . x = f1 . (f . x) ) by A4, FUNCT_1:def 5;
hence g . x in f . x by A3; :: thesis: verum

end;

hence contradiction by A1, A4, Def5; :: thesis: verum

end;

hence contradiction by A2; :: thesis: verum

end;

assume {} in rng f ; :: thesis: product f = {}
then consider x being set such that
A5: ( x in dom f & {} = f . x ) by FUNCT_1:def 5;
assume A6: product f <> {} ; :: thesis: contradiction
consider y being Element of product f;
consider g being Function such that
A7: ( y = g & dom g = dom f & ( for x being set st x in dom f holds
g . x in f . x ) ) by A6, Def5;
thus contradiction by A5, A7; :: thesis: verum