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