let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: - (Sum (<*> the carrier of V)) = 0. V
thus - (Sum (<*> the carrier of V)) = - (0. V) by Lm4
.= 0. V ; :: thesis: verum