Description: The multiplication operation of the extended real number structure. (Contributed by Mario Carneiro, 21-Aug-2015)