theorem Th3: :: RATFUNC1:3

for L being non empty right_complementable right-distributive add-associative right_zeroed unital associative commutative doubleLoopStr
for f being FinSequence of L
for i being Element of NAT st i in dom f holds
Product f = (f /. i) * (Product (Del (f,i)))