for a, b being Complex holds (a * (b ")) " = (a ") * b by Lm11;