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 that
A1: product f = {} and
A2: not {} in rng f ; :: thesis: contradiction

A3: now :: thesis: not dom f = {}

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

end;

now :: thesis: not dom f <> {}

assume dom f <> {} ; :: thesis: contradiction
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: for x being object st x in dom f holds
g . x in f . x

let x be object ; :: thesis: ( x in dom f implies g . x in f . x )
assume A6: x in dom f ; :: thesis: g . x in f . x
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: verum

end;

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

end;

hence contradiction by A3; :: thesis: verum

end;

assume {} in rng f ; :: thesis: product f = {}
then A8: ex x being object st
( x in dom f & {} = f . x ) by FUNCT_1:def 3;
assume A9: product f <> {} ; :: thesis: contradiction
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: verum