let K be comRing; :: thesis: for a1, a2 being Element of K holds (a1 + a2) * (a1 - a2) = (a1 |^ 2) - (a2 |^ 2)
let a1, a2 be Element of K; :: thesis: (a1 + a2) * (a1 - a2) = (a1 |^ 2) - (a2 |^ 2)
thus (a1 + a2) * (a1 - a2) = (a1 * (a1 - a2)) + (a2 * (a1 - a2)) by VECTSP_1:def 7
.= ((a1 * a1) - (a1 * a2)) + (a2 * (a1 - a2)) by VECTSP_1:11
.= ((a1 |^ 2) - (a1 * a2)) + (a2 * (a1 - a2)) by GROUP_1:51
.= ((a1 |^ 2) - (a1 * a2)) + ((a2 * a1) - (a2 * a2)) by VECTSP_1:11
.= ((a1 |^ 2) - (a1 * a2)) + ((a1 * a2) - (a2 |^ 2)) by GROUP_1:51
.= (a1 |^ 2) + ((- (a1 * a2)) + ((a1 * a2) - (a2 |^ 2))) by ALGSTR_1:7
.= (a1 |^ 2) + (((- (a1 * a2)) + (a1 * a2)) - (a2 |^ 2)) by ALGSTR_1:7
.= (a1 |^ 2) + ((0. K) - (a2 |^ 2)) by VECTSP_1:19
.= (a1 |^ 2) - (a2 |^ 2) by VECTSP_1:18 ; :: thesis: verum