Description: Ordinal multiplication with zero. Definition 8.15 of TakeutiZaring
p. 62. Unlike om0 , this version works whether or not A is an
ordinal. However, since it is an artifact of our particular function
value definition outside the domain, we will not use it in order to be
conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996)(New usage is discouraged.)