let V be non empty right_complementable Abelian add-associative right_zeroed CLSStruct ; :: thesis: Sum (ZeroCLC V) = 0. V
consider F being FinSequence of the carrier of V such that
F is one-to-one and
A1: rng F = Carrier (ZeroCLC V) and
A2: Sum (ZeroCLC V) = Sum ((ZeroCLC V) (#) F) by Def6;
F = {} by A1, RELAT_1:41;
then len ((ZeroCLC V) (#) F) = 0 by Def5, CARD_1:27;
hence Sum (ZeroCLC V) = 0. V by A2, RLVECT_1:75; :: thesis: verum