let n be Ordinal; :: thesis: for i being Element of NAT
for b being bag of n st i in dom (decomp b) holds
ex b1, b2 being bag of n st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
let i be Element of NAT ; :: thesis: for b being bag of n st i in dom (decomp b) holds
ex b1, b2 being bag of n st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
let b be bag of n; :: thesis: ( i in dom (decomp b) implies ex b1, b2 being bag of n st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) )
reconsider p = (divisors b) /. i as bag of n ;
assume A1: i in dom (decomp b) ; :: thesis: ex b1, b2 being bag of n st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
take p ; :: thesis: ex b2 being bag of n st
( (decomp b) /. i = <*p,b2*> & b = p + b2 )
take b -' p ; :: thesis: ( (decomp b) /. i = <*p,(b -' p)*> & b = p + (b -' p) )
thus (decomp b) /. i = <*p,(b -' p)*> by A1, Def16; :: thesis: b = p + (b -' p)
i in dom (divisors b) by A1, Def16;
hence b = p + (b -' p) by Th46, Th62; :: thesis: verum