dom (product" {{}}) = DOM {{}} by Def12
.= {} by Th72 ;
hence product" {{}} = {} ; :: thesis: verum