let R be non empty right_complementable well-unital distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for F being FinSequence of R st ex i being Nat st
( i in dom F & F . i = 0. R ) holds
Product F = 0. R
let m be FinSequence of R; :: thesis: ( ex i being Nat st
( i in dom m & m . i = 0. R ) implies Product m = 0. R )
given i being Nat such that A: ( i in dom m & m . i = 0. R ) ; :: thesis: Product m = 0. R
m /. i = m . i by A, PARTFUN1:def 6;
hence Product m = 0. R by A, POLYNOM2:4; :: thesis: verum