for f, F being sequence of NAT st f is multiplicative & ( for n0 being non zero Nat holds F . n0 = Sum (f | (NatDivisors n0)) ) holds
F is multiplicative