theorem :: FUNCT_7:17
{} * = {{}}