let a, b, c be Real; :: thesis: ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)
((a - b) + c) |^ (1 + 1) = (((a - b) + c) |^ 1) * ((a - b) + c) by NEWTON:6
.= ((a - b) + c) * ((a - b) + c)
.= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b * b)) + (b * c))) + (((a * c) - (c * b)) + (c * c))
.= ((((a * a) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c * c)) by WSIERP_1:1
.= ((((a |^ 2) - (a * b)) + (a * c)) - (((a * b) - (b |^ 2)) + (b * c))) + (((a * c) - (c * b)) + (c |^ 2)) by WSIERP_1:1
.= (((((a |^ 2) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c)) + (b |^ 2) ;
hence ((a - b) + c) |^ 2 = (((((a |^ 2) + (b |^ 2)) + (c |^ 2)) - ((2 * a) * b)) + ((2 * a) * c)) - ((2 * b) * c) ; :: thesis: verum