let n be Ordinal; :: thesis: for b, b1, b2 being bag of n st b = b1 + b2 holds
ex i being Element of NAT st
( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )
let b, b1, b2 be bag of n; :: thesis: ( b = b1 + b2 implies ex i being Element of NAT st
( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) )
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: BagOrder n linearly_orders S by Lm4, ORDERS_1:38;
assume A4: b = b1 + b2 ; :: thesis: ex i being Element of NAT st
( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )
then b1 divides b by Th49;
then b1 in S by A2;
then b1 in rng (divisors b) by A1, A3, Def2;
then consider i being Element of NAT such that
A5: i in dom (divisors b) and
A6: (divisors b) /. i = b1 by PARTFUN2:2;
take i ; :: thesis: ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> )
thus i in dom (decomp b) by A5, Def16; :: thesis: (decomp b) /. i = <*b1,b2*>
then (decomp b) /. i = <*b1,(b -' b1)*> by A6, Def16;
hence (decomp b) /. i = <*b1,b2*> by A4, Th47; :: thesis: verum