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