theorem :: EC_PF_2:16

for K being comRing
for a1, a2 being Element of K holds (a1 + a2) * (((a1 |^ 2) - (a1 * a2)) + (a2 |^ 2)) = (a1 |^ 3) + (a2 |^ 3)