let m be multiplicative-trivial integer-yielding FinSequence; :: thesis: Product m = 0
ex i being natural number st
( i in dom m & m . i = 0 ) by Def1;
hence Product m = 0 by Th6; :: thesis: verum