theorem Th25: :: POLYALGX:25

for b being bag of 1 holds
( SgmX ((BagOrder 1),(rng (divisors b))) = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) & divisors b = XFS2FS (NBag1 | (Segm ((b . 0) + 1))) )