let x, y be real number ; :: 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