let F be Field; :: thesis: for a, b, c, d being Element of F holds (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
let a, b, c, d be Element of F; :: thesis: (a - b) * (c - d) = (a * c) + ((- (a * d)) + (- (b * (c - d))))
thus (a - b) * (c - d) = (a + (- b)) * (c - d) by RLVECT_1:def 11
.= (a * (c - d)) + ((- b) * (c - d)) by VECTSP_1:def 7
.= (a * (c - d)) + (- (b * (c - d))) by VECTSP_1:9
.= ((a * c) - (a * d)) + (- (b * (c - d))) by VECTSP_1:11
.= ((a * c) + (- (a * d))) + (- (b * (c - d))) by RLVECT_1:def 11
.= (a * c) + ((- (a * d)) + (- (b * (c - d)))) by RLVECT_1:def 3 ; :: thesis: verum