let n be Ordinal; :: thesis: for b being bag of n holds
( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )
let b be bag of n; :: thesis: ( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )
consider S being non empty finite Subset of (Bags n) such that
A1: divisors b = SgmX ((BagOrder n),S) and
A2: for p being bag of n holds
( p in S iff p divides b ) by Def15;
A3: now :: thesis: for y being Element of Bags n st y in S holds
[y,b] in BagOrder n
let y be Element of Bags n; :: thesis: ( y in S implies [y,b] in BagOrder n )
assume y in S ; :: thesis: [y,b] in BagOrder n
then y divides b by A2;
then y <=' b by Th48;
hence [y,b] in BagOrder n by Def13; :: thesis: verum
end;
A4: now :: thesis: for y being Element of Bags n st y in S holds
[(EmptyBag n),y] in BagOrder n
let y be Element of Bags n; :: thesis: ( y in S implies [(EmptyBag n),y] in BagOrder n )
assume y in S ; :: thesis: [(EmptyBag n),y] in BagOrder n
EmptyBag n <=' y by Th48, Th57;
hence [(EmptyBag n),y] in BagOrder n by Def13; :: thesis: verum
end;
A5: BagOrder n linearly_orders S by Lm4, ORDERS_1:38;
EmptyBag n divides b ;
then EmptyBag n in S by A2;
hence (divisors b) /. 1 = EmptyBag n by A1, A5, A4, Th19; :: thesis: (divisors b) /. (len (divisors b)) = b
b in S by A2;
hence (divisors b) /. (len (divisors b)) = b by A1, A5, A3, Th20; :: thesis: verum