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