let a, b be Complex; :: thesis: (a / (2 * b)) + (a / (2 * b)) = a / b
thus (a / (2 * b)) + (a / (2 * b)) = (a + a) / (2 * b) by Th62
.= (2 * a) / (2 * b)
.= a / b by Lm10 ; :: thesis: verum