let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for v, w being Element of V holds Sum <*(- v),(- w)*> = - (w + v)
let v, w be Element of V; :: thesis: Sum <*(- v),(- w)*> = - (w + v)
thus Sum <*(- v),(- w)*> = (- v) + (- w) by Th45
.= - (w + v) by Lm3 ; :: thesis: verum