let n be Nat; :: thesis: ((2 * n) + 1) |^ 2 = ((4 * n) * (n + 1)) + 1
thus ((2 * n) + 1) |^ 2 = ((2 * n) + 1) * ((2 * n) + 1) by NEWTON:81
.= ((4 * n) * (n + 1)) + 1 ; :: thesis: verum