theorem :: FUNCT_7:17

{} * = {{}}