let n be Ordinal; :: thesis: for b being bag of holds
( (divisors b) /. 1 = EmptyBag n & (divisors b) /. (len (divisors b)) = b )
let b be bag of ; :: 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 holds
( p in S iff p divides b ) by Def18;
EmptyBag n divides b by Th63;
then A3: EmptyBag n in S by A2;
A4: BagOrder n linearly_orders S by Lm4, ORDERS_1:134;

now

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 Th53, Th63;
hence [(EmptyBag n),y] in BagOrder n by Def16; :: thesis: verum

end;

hence (divisors b) /. 1 = EmptyBag n by A1, A3, A4, Th8; :: thesis: (divisors b) /. (len (divisors b)) = b
A5: b in S by A2;

now

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 Th53;
hence [y,b] in BagOrder n by Def16; :: thesis: verum

end;

hence (divisors b) /. (len (divisors b)) = b by A1, A4, A5, Th9; :: thesis: verum