let a, b be Complex; :: thesis: (a * (b ")) " = (a ") * b
thus (a * (b ")) " = (a ") * ((b ") ") by Lm1
.= (a ") * b ; :: thesis: verum