for c, c9 being Element of COMPLEX holds (c multcomplex) . c9 = c * c9 by Lm3;