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 Th59
.= - (Sum <*v,v*>) by Th45
.= - (2 * v) by Th60
.= (- 1) * (2 * v) by Th16
.= ((- 1) * 2) * v by Def7
.= (- 2) * v ; :: thesis: verum