let V be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: - (0. V) = 0. V
thus 0. V = (0. V) + (- (0. V)) by Def13
.= - (0. V) by Th10 ; :: thesis: verum