let x, y be Real; :: thesis: (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2))
(((x ^2) - (x * y)) + (y ^2)) * (x + y) = ((((x ^2) * x) + (y * (x ^2))) - ((x * (x * y)) + (y * (x * y)))) + (((x * (y ^2)) + (y * (y ^2))) + (0 * (y ^2)))
.= (((x |^ 3) + (y * (x ^2))) - ((x * (x * y)) + (y * (x * y)))) + ((x * (y ^2)) + (y * (y ^2))) by POLYEQ_2:4
.= (((x |^ 3) + (y * (x ^2))) - (((x ^2) * y) + ((y * y) * x))) + ((x * (y ^2)) + (y |^ 3)) by POLYEQ_2:4
.= (x |^ 3) + (y |^ 3) ;
hence (x |^ 3) + (y |^ 3) = (x + y) * (((x ^2) - (x * y)) + (y ^2)) ; :: thesis: verum