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