theorem prod5: :: RING_2:2

for R being non degenerated right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for F being FinSequence of R holds
( Product F = 0. R iff ex i being Nat st
( i in dom F & F . i = 0. R ) )