theorem Th16: :: NAT_3:16

for a being Nat
for X being set
for b being real-valued ManySortedSet of X st a <> 0 holds
support b = support (a * b)