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