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