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