let x, y be Real; :: thesis: (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2) + (x * y)) + (y ^2))
(x - y) * (((x ^2) + (x * y)) + (y ^2)) = (((x * (x ^2)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2)))
.= (((x * (x |^ 2)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2))) by NEWTON:81
.= (((x |^ (2 + 1)) + ((x * x) * y)) + (x * (y ^2))) - (((y * (x ^2)) + ((y * x) * y)) + (y * (y ^2))) by NEWTON:6
.= (((x |^ 3) + (x * (y * y))) - ((y * x) * y)) - (y * (y ^2))
.= (x |^ 3) - ((y |^ 2) * y) by NEWTON:81
.= (x |^ 3) - (y |^ (2 + 1)) by NEWTON:6 ;
hence (x |^ 3) - (y |^ 3) = (x - y) * (((x ^2) + (x * y)) + (y ^2)) ; :: thesis: verum