let n be Ordinal; :: thesis: for i being Element of NAT
for b, b1, b2 being bag of st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds
b1 = (divisors b) /. i
let i be Element of NAT ; :: thesis: for b, b1, b2 being bag of st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds
b1 = (divisors b) /. i
let b, b1, b2 be bag of ; :: thesis: ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> implies b1 = (divisors b) /. i )
reconsider p = (divisors b) /. i as bag of by Def14;
assume ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) ; :: thesis: b1 = (divisors b) /. i
then <*b1,b2*> = <*p,(b -' p)*> by Def19;
hence b1 = (divisors b) /. i by GROUP_7:2; :: thesis: verum