let K be comRing; :: thesis: for a1, a2 being Element of K holds (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) + (a2 |^ 3)
let a1, a2 be Element of K; :: thesis: (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) + (a2 |^ 3)
thus (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2))) + (a2 * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:def 7
.= ((a1 * ((a1 |^ 2) - (a1 * a2))) + (a1 * (a2 |^ 2))) + (a2 * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:def 7
.= (((a1 * (a1 |^ 2)) - (a1 * (a1 * a2))) + (a1 * (a2 |^ 2))) + (a2 * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2))) by VECTSP_1:11
.= ((((a1 |^ 2) * a1) - ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) + (a2 * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2))) by GROUP_1:def 3
.= ((((a1 |^ 2) * a1) - ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) + ((a2 * ((a1 |^ 2) - (a1 * a2))) + (a2 * (a2 |^ 2))) by VECTSP_1:def 7
.= (((a1 |^ (2 + 1)) - ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) + ((a2 * ((a1 |^ 2) - (a1 * a2))) + ((a2 |^ 2) * a2)) by EC_PF_1:24
.= (((a1 |^ 3) - ((a1 * a1) * a2)) + (a1 * (a2 |^ 2))) + (((a2 * (a1 |^ 2)) - (a2 * (a1 * a2))) + ((a2 |^ 2) * a2)) by VECTSP_1:11
.= (((a1 |^ 3) - ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) + (((a2 * (a1 |^ 2)) - (a2 * (a1 * a2))) + ((a2 |^ 2) * a2)) by GROUP_1:51
.= (((a1 |^ 3) - ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) + ((((a1 |^ 2) * a2) - ((a1 * a2) * a2)) + (a2 |^ (2 + 1))) by EC_PF_1:24
.= (((a1 |^ 3) - ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2))) + ((((a1 |^ 2) * a2) - (a1 * (a2 * a2))) + (a2 |^ 3)) by GROUP_1:def 3
.= ((a1 |^ 3) + ((- ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2)))) + ((((a1 |^ 2) * a2) - (a1 * (a2 * a2))) + (a2 |^ 3)) by ALGSTR_1:7
.= ((a1 |^ 3) + ((- ((a1 |^ 2) * a2)) + (a1 * (a2 |^ 2)))) + ((((a1 |^ 2) * a2) - (a1 * (a2 |^ 2))) + (a2 |^ 3)) by GROUP_1:51
.= (((a1 |^ 3) + ((a1 * (a2 |^ 2)) - ((a1 |^ 2) * a2))) + (((a1 |^ 2) * a2) - (a1 * (a2 |^ 2)))) + (a2 |^ 3) by ALGSTR_1:8
.= ((a1 |^ 3) + (((a1 * (a2 |^ 2)) - ((a1 |^ 2) * a2)) + (((a1 |^ 2) * a2) - (a1 * (a2 |^ 2))))) + (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + ((((a1 * (a2 |^ 2)) - ((a1 |^ 2) * a2)) + ((a1 |^ 2) * a2)) - (a1 * (a2 |^ 2)))) + (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + (((a1 * (a2 |^ 2)) + ((- ((a1 |^ 2) * a2)) + ((a1 |^ 2) * a2))) - (a1 * (a2 |^ 2)))) + (a2 |^ 3) by ALGSTR_1:7
.= ((a1 |^ 3) + (((a1 * (a2 |^ 2)) + (0. K)) - (a1 * (a2 |^ 2)))) + (a2 |^ 3) by VECTSP_1:19
.= ((a1 |^ 3) + (0. K)) + (a2 |^ 3) by VECTSP_1:19, ALGSTR_1:7
.= (a1 |^ 3) + (a2 |^ 3) by ALGSTR_1:7 ; :: thesis: verum