:: deftheorem defines multiplicative NAT_5:def 5 :
for f being sequence of NAT holds
( f is multiplicative iff for n0, m0 being non zero Nat st n0,m0 are_coprime holds
f . (n0 * m0) = (f . n0) * (f . m0) );