theorem :: FUNCT_7:16

INT <> INT *