let a1, b1 be Complex; :: thesis: (a1 |^ 3) - (b1 |^ 3) = (a1 - b1) * (((a1 |^ 2) + (b1 |^ 2)) + (a1 * b1))
(a1 |^ (2 + 1)) - (b1 |^ (2 + 1)) = ((a1 |^ 2) * ((a1 |^ 1) - (b1 |^ 1))) + ((b1 |^ 1) * ((a1 |^ 2) - (b1 |^ 2))) by RI2
.= ((a1 |^ 2) * (a1 - b1)) + (b1 * ((a1 + b1) * (a1 - b1))) by NEWTON01:1
.= (a1 - b1) * (((a1 |^ 2) + (b1 * b1)) + (a1 * b1)) ;
hence (a1 |^ 3) - (b1 |^ 3) = (a1 - b1) * (((a1 |^ 2) + (b1 |^ 2)) + (a1 * b1)) by NEWTON:81; :: thesis: verum