let V be non empty Abelian add-associative right_zeroed addLoopStr ; :: thesis: Sum ({} V) = 0. V
Sum (<*> the carrier of V) = 0. V by RLVECT_1:43;
hence Sum ({} V) = 0. V by Def2, RELAT_1:38; :: thesis: verum