:: deftheorem Def1 defines multiplicative-trivial INT_6:def 1 :
for f being INT -valued FinSequence holds
( not f is multiplicative-trivial iff for i being Nat holds
( not i in dom f or not f . i = 0 ) );