theorem Th25: :: NUMBER08:25

for s, t being non zero Nat st s,t are_coprime holds
(EmptyBag SetPrimes) +* (Euler_factorization (s * t)) = ((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t))