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