let f, g be Function; :: thesis: ( product f = product g & f is non-empty implies g is non-empty )
assume A1: product f = product g ; :: thesis: ( not f is non-empty or g is non-empty )

now :: thesis: ( f is non-empty implies g is non-empty )

assume that
A2: f is non-empty and
A3: not g is non-empty ; :: thesis: contradiction
ex n being object st
( n in dom g & g . n is empty ) by A3, FUNCT_1:def 9;
then {} in rng g by FUNCT_1:def 3;
then product g = {} by CARD_3:26;
then {} in rng f by A1, CARD_3:26;
then ex n being object st
( n in dom f & f . n = {} ) by FUNCT_1:def 3;
hence contradiction by A2, FUNCT_1:def 9; :: thesis: verum

end;

hence ( not f is non-empty or g is non-empty ) ; :: thesis: verum