let F be Field; :: thesis: for c1, c2 being Element of F holds <%(- c1),(1. F)%> *' <%(- c2),(1. F)%> = <%(c1 * c2),(- (c1 + c2)),(1. F)%>
let c1, c2 be Element of F; :: thesis: <%(- c1),(1. F)%> *' <%(- c2),(1. F)%> = <%(c1 * c2),(- (c1 + c2)),(1. F)%>
thus <%(- c1),(1. F)%> *' <%(- c2),(1. F)%> = <%((- c1) * (- c2)),(((1. F) * (- c2)) + ((1. F) * (- c1))),((1. F) * (1. F))%> by lemred1
.= <%(c1 * c2),((- c2) + (- c1)),(1. F)%> by VECTSP_1:10
.= <%(c1 * c2),(- (c1 + c2)),(1. F)%> by RLVECT_1:31 ; :: thesis: verum