begin
Lm1:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V ex w being Element of V st v + w = u
Lm3:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, w being Element of V holds - (u + w) = (- w) + (- u)
Lm4:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm5:
for V being non empty addLoopStr
for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds
Sum F = 0. V
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v
begin
begin