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