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) & Sum (ZeroCLC V) = Sum ((ZeroCLC V) (#) F) ) by Def5;
F = {} by A1, RELAT_1:64;
then len ((ZeroCLC V) (#) F) = 0 by Def4, CARD_1:47;
hence Sum (ZeroCLC V) = 0. V by A1, RLVECT_1:94; :: thesis: verum