theorem Th14: :: POLYEQ_1:14
for h, y being Real holds (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)