for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being FinSequence of the carrier of L st ex i being Element of NAT st
( i in dom p & p /. i = 0. L ) holds
Product p = 0. L