let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for v, u being Element of V holds - (Sum <*v,u*>) = (- v) - u
let v, u be Element of V; :: thesis: - (Sum <*v,u*>) = (- v) - u
thus - (Sum <*v,u*>) = - (v + u) by RLVECT_1:62
.= (- v) - u by VECTSP_1:64 ; :: thesis: verum