let R be commutative Ring; :: thesis: for a, b being Element of R holds (a + b) * (a - b) = (a ^2) - (b ^2)
let a, b be Element of R; :: thesis: (a + b) * (a - b) = (a ^2) - (b ^2)
thus (a + b) * (a - b) = (a * (a - b)) + (b * (a - b)) by VECTSP_1:def 7
.= ((a * a) + (a * (- b))) + (b * (a + (- b))) by VECTSP_1:def 7
.= ((a * a) + (a * (- b))) + ((b * a) + (b * (- b))) by VECTSP_1:def 7
.= (a * a) + ((a * (- b)) + ((b * a) + (b * (- b)))) by RLVECT_1:def 3
.= (a * a) + (((a * (- b)) + (b * a)) + (b * (- b))) by RLVECT_1:def 3
.= (a * a) + (((- (a * b)) + (b * a)) + (b * (- b))) by VECTSP_1:8
.= (a * a) + ((0. R) + (b * (- b))) by RLVECT_1:5
.= (a ^2) - (b ^2) by VECTSP_1:8 ; :: thesis: verum