let a be Real; :: thesis: (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1
(a + 1) |^ 3 = ((a + 1) |^ 2) * (a + 1) by Lm2
.= (((a |^ 2) + ((2 * a) * 1)) + (1 |^ 2)) * (a + 1) by Lm3
.= (((a |^ 2) + (2 * a)) + 1) * (a + 1)
.= ((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + (2 * a))) + ((1 * a) + (1 * 1))
.= ((((a |^ 2) * a) + ((a |^ 2) * 1)) + (((2 * a) * a) + ((2 * a) * 1))) + (((1 |^ 2) * a) + 1)
.= (((a |^ (2 + 1)) + (a |^ 2)) + (((2 * a) * a) + (2 * a))) + (((1 |^ 2) * a) + 1) by NEWTON:6
.= (((a |^ 3) + (a |^ 2)) + ((2 * (a * a)) + (2 * a))) + ((1 * a) + 1)
.= (((a |^ 3) + (a |^ 2)) + ((2 * ((a |^ 1) * a)) + (2 * a))) + (a + 1)
.= (((a |^ 3) + (a |^ 2)) + ((2 * (a |^ (1 + 1))) + (2 * a))) + (a + 1) by NEWTON:6
.= ((((a |^ 3) + (a |^ 2)) + (2 * (a |^ 2))) + (2 * a)) + (a + 1) ;
hence (a + 1) |^ 3 = (((a |^ 3) + (3 * (a |^ 2))) + (3 * a)) + 1 ; :: thesis: verum