let n be Ordinal; :: thesis: divisors (EmptyBag n) = <*(EmptyBag n)*>
consider S being non empty finite Subset of (Bags n) such that
A1: divisors (EmptyBag n) = SgmX ((BagOrder n),S) and
A2: for p being bag of n holds
( p in S iff p divides EmptyBag n ) by Def15;
A3: S c= {(EmptyBag n)}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in S or x in {(EmptyBag n)} )
assume A4: x in S ; :: thesis: x in {(EmptyBag n)}
then reconsider b = x as bag of n ;
b divides EmptyBag n by A2, A4;
then b = EmptyBag n ;
hence x in {(EmptyBag n)} by TARSKI:def 1; :: thesis: verum
end;
A5: BagOrder n linearly_orders S by Lm4, ORDERS_1:38;
EmptyBag n in S by A2;
then {(EmptyBag n)} c= S by ZFMISC_1:31;
then S = {(EmptyBag n)} by A3;
then A6: rng (divisors (EmptyBag n)) = {(EmptyBag n)} by A1, A5, Def2;
len (divisors (EmptyBag n)) = card (rng (divisors (EmptyBag n))) by Th18
.= 1 by A6, CARD_1:30 ;
hence divisors (EmptyBag n) = <*(EmptyBag n)*> by A6, FINSEQ_1:39; :: thesis: verum