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 * (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 ^2) + (((a * b) + (b * a)) + (b * b)) by RLVECT_1:def 3
.= (a ^2) + ((2 '*' (a * b)) + (b ^2)) by RING_5:2
.= ((a ^2) + (2 '*' (a * b))) + (b ^2) by RLVECT_1:def 3
.= ((a ^2) + ((2 '*' a) * b)) + (b ^2) by c1 ; :: thesis: verum