theorem Th24: :: NUMBER16:24

for n, m being non zero Nat st n,m are_coprime holds
rng (pfexp (n * m)) = (rng (pfexp n)) \/ (rng (pfexp m))