theorem :: NUMBER19:60

for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for z being FinSequence of the carrier of L
for i being Nat st not i in dom z holds
LagIPoly (z,i) = Product (rpoly (((len z) |-> 1),z))