for o1, o2 being Ordinal
for b1 being Element of Bags o1
for b2 being Element of Bags o2
for G being FinSequence of (Bags (o1 +^ o2)) * st dom G = dom (divisors b1) & ( for i being Nat st i in dom (divisors b1) holds
ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a19 & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) ) ) ) holds
divisors (b1 +^ b2) = FlattenSeq G