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

assume A2: ( f is non-empty & not g is non-empty ) ; :: thesis: contradiction
then consider n being set such that
A3: ( n in dom g & g . n is empty ) by FUNCT_1:def 15;
{} in rng g by A3, FUNCT_1:def 5;
then product g = {} by CARD_3:37;
then {} in rng f by A1, CARD_3:37;
then consider n being set such that
A4: ( n in dom f & f . n = {} ) by FUNCT_1:def 5;
thus contradiction by A2, A4, FUNCT_1:def 15; :: thesis: verum

end;

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