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

proof

assume that
A1: product f = {} and
A2: not {} in rng f ; :: thesis:

A3: now :: thesis:

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

end;

now :: thesis:

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

now :: thesis:

let x be object ; :: thesis:
assume A6: x in dom f ; :: thesis:
then A7: f . x in M by FUNCT_1:def 3;
g . x = f1 . (f . x) by A5, A6;
hence g . x in f . x by A4, A7; :: thesis:

end;

hence contradiction by A1, A5, Def5; :: thesis:

end;

hence contradiction by A3; :: thesis:

end;

assume {} in rng f ; :: thesis:
then A8: ex x being object st
( x in dom f & {} = f . x ) by FUNCT_1:def 3;
assume A9: product f <> {} ; :: thesis:
set y = the Element of product f;
ex g being Function st
( the Element of product f = g & dom g = dom f & ( for x being object st x in dom f holds
g . x in f . x ) ) by A9, Def5;
hence contradiction by A8; :: thesis: