let f be integer-yielding FinSequence; :: thesis: ( f is multiplicative-trivial implies not f is empty )
assume f is multiplicative-trivial ; :: thesis: not f is empty
then consider i being natural number such that
A: ( i in dom f & f . i = 0 ) by DefMTriv;
thus not f is empty by A; :: thesis: verum