let m be multiplicative-trivial integer-yielding FinSequence; :: thesis: Product m = 0
consider i being natural number such that
A: ( i in dom m & m . i = 0 ) by DefMTriv;
thus Product m = 0 by A, mtriv; :: thesis: verum