let a1, b1, c1, d1 be Complex; :: thesis: ( a1 + (b1 |^ 2) = c1 |^ 2 implies (a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2) = (2 * d1) * (b1 - c1) )
assume A1: a1 + (b1 |^ 2) = c1 |^ 2 ; :: thesis: (a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2) = (2 * d1) * (b1 - c1)
(a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2) = (a1 + (((b1 |^ 2) + ((2 * b1) * d1)) + (d1 |^ 2))) - ((c1 + d1) |^ 2) by Lm10
.= (((a1 + (b1 |^ 2)) + ((2 * b1) * d1)) + (d1 |^ 2)) - (((c1 |^ 2) + ((2 * c1) * d1)) + (d1 |^ 2)) by Lm10
.= ((2 * b1) * d1) - ((2 * c1) * d1) by A1 ;
hence (a1 + ((b1 + d1) |^ 2)) - ((c1 + d1) |^ 2) = (2 * d1) * (b1 - c1) ; :: thesis: verum