let n be Nat; :: thesis:
((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = (((n + 1) |^ 2) * (2 * ((n + 1) |^ 2))) - (((n + 1) |^ 2) * 1)
.= ((((n + 1) |^ 2) * ((n + 1) |^ 2)) * 2) - (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) by Lm3
.= ((((n + 1) |^ 2) * ((n + 1) |^ 2)) * 2) - (((n |^ 2) + (2 * n)) + 1)
.= ((((n + 1) |^ 2) * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) * 2) - (((n |^ 2) + (2 * n)) + 1) by Lm3
.= (((((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2)) * (((n |^ 2) + (2 * n)) + (1 |^ 2))) * 2) - (((n |^ 2) + (2 * n)) + 1) by Lm3
.= (((((n |^ 2) + (2 * n)) + (1 |^ 2)) * (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1)
.= (((((n |^ 2) + (2 * n)) + 1) * (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1)
.= (((((((n |^ 2) * (n |^ 2)) + ((2 * n) * (n |^ 2))) + (n |^ 2)) + ((((2 * n) * (n |^ 2)) + (((2 * n) * n) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1)
.= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ (2 + 1)))) + (n |^ 2)) + (((2 * (n * (n |^ 2))) + ((2 * (n * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6
.= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ (2 + 1)))) + (n |^ 2)) + (((2 * (n |^ (2 + 1))) + ((2 * (n * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6
.= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * ((n |^ 1) * n)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1)
.= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * (n |^ (1 + 1))) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) by NEWTON:6
.= (((((((n |^ 2) * (n |^ 2)) + (2 * (n |^ 3))) + (n |^ 2)) + (((2 * (n |^ 3)) + ((2 * (n |^ 2)) * 2)) + (2 * n))) + (((n |^ 2) + (2 * n)) + 1)) * 2) - (((n |^ 2) + (2 * n)) + 1) ;
hence ((n + 1) |^ 2) * ((2 * ((n + 1) |^ 2)) - 1) = ((((((n |^ 2) * (n |^ 2)) * 2) + ((12 - 1) * (n |^ 2))) + (8 * (n |^ 3))) + (6 * n)) + 1 ; :: thesis: