theorem Th46: :: NAT_3:46

for a, b being non zero Nat holds support (pfexp (a * b)) = (support (pfexp a)) \/ (support (pfexp b))