theorem Th20: :: NAT_3:20

for A being set holds Product (EmptyBag A) = 1