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