let a, b be Complex; :: thesis: (a - b) |^ 2 = ((a |^ 2) - ((2 * a) * b)) + (b |^ 2)
thus (a - b) |^ 2 = (a - b) * (a - b) by Th1
.= ((a ^2) - ((2 * a) * b)) + (b ^2)
.= ((a |^ 2) - ((2 * a) * b)) + (b * b) by Th1
.= ((a |^ 2) - ((2 * a) * b)) + (b |^ 2) by Th1 ; :: thesis: verum