theorem Th17: :: EC_PF_2:17

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