let a1 be Complex; :: thesis: (((2 * a1) + 1) |^ 2) + (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) = (((2 * (a1 |^ 2)) + (2 * a1)) + 1) |^ 2
(((2 * (a1 |^ 2)) + (2 * a1)) + 1) |^ 2 = (((2 * (a1 |^ 2)) + (2 * a1)) + 1) * (((2 * (a1 |^ 2)) + (2 * a1)) + 1) by NEWTON:81
.= ((((((2 * (a1 |^ 2)) * (2 * (a1 |^ 2))) + ((2 * a1) * (2 * a1))) + 1) + ((2 * (2 * a1)) * (2 * (a1 |^ 2)))) + (2 * (2 * (a1 |^ 2)))) + (2 * (2 * a1))
.= ((((((2 * (a1 |^ 2)) |^ 2) + ((2 * a1) * (2 * a1))) + 1) + ((2 * (2 * a1)) * (2 * (a1 |^ 2)))) + (2 * (2 * (a1 |^ 2)))) + (2 * (2 * a1)) by NEWTON:81
.= ((((((2 * (a1 |^ 2)) |^ 2) + ((2 * a1) |^ 2)) + 1) + ((2 * (2 * (a1 |^ 2))) * (2 * a1))) + (2 * (2 * (a1 |^ 2)))) + ((2 * (2 * a1)) * 1) by NEWTON:81
.= ((((2 * (a1 |^ 2)) |^ 2) + ((2 * (2 * (a1 |^ 2))) * (2 * a1))) + ((2 * a1) |^ 2)) + ((((2 * 2) * (a1 |^ 2)) + ((2 * (2 * a1)) * 1)) + (1 |^ 2))
.= (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) + ((((2 * 2) * (a1 |^ 2)) + ((2 * (2 * a1)) * 1)) + (1 |^ 2)) by Lm10
.= (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) + ((((2 |^ 2) * (a1 |^ 2)) + ((2 * (2 * a1)) * 1)) + (1 |^ 2)) by NEWTON:81
.= (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) + ((((2 * a1) |^ 2) + ((2 * (2 * a1)) * 1)) + (1 |^ 2)) by NEWTON:7 ;
hence (((2 * a1) + 1) |^ 2) + (((2 * (a1 |^ 2)) + (2 * a1)) |^ 2) = (((2 * (a1 |^ 2)) + (2 * a1)) + 1) |^ 2 by Lm10; :: thesis: verum