let n be Ordinal; :: thesis: for i being Element of NAT
for b, b1, b2 being bag of n 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 n st i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> holds
b1 = (divisors b) /. i
let b, b1, b2 be bag of n; :: thesis: ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> implies b1 = (divisors b) /. i )
reconsider p = (divisors b) /. i as bag of n ;
assume ( i in dom (decomp b) & (decomp b) /. i = <*b1,b2*> ) ; :: thesis: b1 = (divisors b) /. i
then <*b1,b2*> = <*p,(b -' p)*> by Def16;
hence b1 = (divisors b) /. i by FINSEQ_1:77; :: thesis: verum