theorem Th62: :: PRE_POLY:64

for n being Ordinal
for i being Element of NAT
for b being bag of n st i in dom (divisors b) holds
(divisors b) /. i divides b