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