begin
Lm1:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for V being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed VectSpStr over GF holds Sum (ZeroLC V) = 0. V
Lm2:
for GF being non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a
Lm3:
for GF being Field holds - (1. GF) <> 0. GF
:: Auxiliary theorems.
::