let x, y be Real; :: thesis: (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3)
(x + y) |^ 3 = ((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3) by POLYEQ_1:14
.= (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) ;
hence (x + y) |^ 3 = (((x |^ 3) + ((3 * (x ^2)) * y)) + ((3 * x) * (y ^2))) + (y |^ 3) ; :: thesis: verum