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 ex i being natural number st
( i in dom f & f . i = 0 ) by Def1;
hence not f is empty ; :: thesis: verum