for K being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive Abelian add-associative right_zeroed doubleLoopStr
for p being FinSequence of the carrier of K holds
( ex k being Nat st
( k in dom p & p . k = 0. K ) iff Product p = 0. K )