now

given x being set such that A1: x in dom (product" {{}}) ; :: thesis: contradiction
{} in {{}} by TARSKI:def 1;
then x in dom {} by A1, Def13;
hence contradiction ; :: thesis: verum

end;

then dom (product" {{}}) = {} by XBOOLE_0:7;
hence product" {{}} = {} ; :: thesis: verum