let n be Ordinal; :: thesis: for i being Element of NAT
for b being bag of st i in dom (decomp b) holds
ex b1, b2 being bag of st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
let i be Element of NAT ; :: thesis: for b being bag of st i in dom (decomp b) holds
ex b1, b2 being bag of st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
let b be bag of ; :: thesis: ( i in dom (decomp b) implies ex b1, b2 being bag of st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 ) )
assume A1: i in dom (decomp b) ; :: thesis: ex b1, b2 being bag of st
( (decomp b) /. i = <*b1,b2*> & b = b1 + b2 )
then A2: i in dom (divisors b) by Def19;
reconsider p = (divisors b) /. i as bag of by Def14;
take p ; :: thesis: ex b2 being bag of 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, Def19; :: thesis: b = p + (b -' p)
thus b = p + (b -' p) by A2, Th51, Th68; :: thesis: verum