theorem Th63: :: PRE_POLY:65

for n being Ordinal
for b being bag of n holds
( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )