let V be RealLinearSpace; :: thesis: for v being VECTOR of V holds Sum <*(- v),(- v)*> = (- 2) * v
let v be VECTOR of V; :: thesis: Sum <*(- v),(- v)*> = (- 2) * v
thus Sum <*(- v),(- v)*> = - (v + v) by Th78
.= - (Sum <*v,v*>) by Th62
.= - (2 * v) by Th79
.= (- 1) * (2 * v) by Th29
.= ((- 1) * 2) * v by Def10
.= (- 2) * v ; :: thesis: verum