let h, y be Real; :: thesis: (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3)
(y + h) |^ 3 = (y + h) |^ (2 + 1) ;
then A1: (y + h) |^ 3 = ((y + h) |^ (1 + 1)) * (y + h) by NEWTON:6
.= (((y + h) |^ 1) * (y + h)) * (y + h) by NEWTON:6
.= ((y + h) |^ 1) * ((y + h) ^2)
.= ((y + h) to_power 1) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:41
.= (y + h) * (((y ^2) + ((2 * y) * h)) + (h ^2)) by POWER:25
.= ((y * (y ^2)) + (((3 * h) * (y ^2)) + (((2 + 1) * (h ^2)) * y))) + (h * (h ^2)) ;
y |^ 3 = y |^ (2 + 1)
.= (y |^ (1 + 1)) * y by NEWTON:6
.= ((y |^ 1) * y) * y by NEWTON:6
.= (y |^ 1) * (y ^2) ;
then A2: y |^ 3 = (y to_power 1) * (y ^2) by POWER:41;
h |^ 3 = h |^ (2 + 1)
.= (h |^ (1 + 1)) * h by NEWTON:6
.= ((h |^ 1) * h) * h by NEWTON:6
.= (h |^ 1) * (h ^2)
.= (h to_power 1) * (h ^2) by POWER:41
.= h * (h ^2) by POWER:25 ;
hence (y + h) |^ 3 = ((y |^ 3) + (((3 * h) * (y ^2)) + ((3 * (h ^2)) * y))) + (h |^ 3) by A1, A2, POWER:25; :: thesis: verum