let R be commutative Ring; :: thesis: for a, b being Element of R holds (a - b) ^2 = ((a ^2) - ((2 '*' a) * b)) + (b ^2)
let a, b be Element of R; :: thesis: (a - b) ^2 = ((a ^2) - ((2 '*' a) * b)) + (b ^2)
thus (a - b) ^2 = ((a ^2) + ((2 '*' a) * (- b))) + ((- b) ^2) by P3
.= ((a ^2) + (2 '*' (a * (- b)))) + ((- b) ^2) by c1
.= ((a ^2) + (2 '*' (- (a * b)))) + ((- b) ^2) by VECTSP_1:8
.= ((a ^2) + (- (2 '*' (a * b)))) + ((- b) ^2) by c1a
.= ((a ^2) - ((2 '*' a) * b)) + ((- b) ^2) by c1
.= ((a ^2) - ((2 '*' a) * b)) + (b ^2) by VECTSP_1:10 ; :: thesis: verum