theorem Th45: :: NAT_3:45

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