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 Th45
.= - (v + w) by Lm3 ; :: thesis: Sum <*(- w),(- v)*> = - (v + w)
hence Sum <*(- w),(- v)*> = - (v + w) by Th54; :: thesis: verum