:: deftheorem defines Sum FVSUM_1:def 8 :
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for p being FinSequence of the carrier of K holds Sum p = the addF of K $$ p;