let o1, o2 be Ordinal; :: thesis: 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

let b1 be Element of Bags o1; :: thesis: 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

let b2 be Element of Bags o2; :: thesis: 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

let G be FinSequence of (Bags (o1 +^ o2)) * ; :: thesis: ( 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 ) ) ) ) implies divisors (b1 +^ b2) = FlattenSeq G )

assume that
A1: dom G = dom (divisors b1) and
A2: 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 ) ) ) ; :: thesis: divisors (b1 +^ b2) = FlattenSeq G
reconsider D = Del (G,1) as FinSequence of (Bags (o1 +^ o2)) * ;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A3: Fk = G /. 1 and
(divisors b1) /. 1 = a19 and
A4: len Fk = len (divisors b2) and
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 ) by ;
len (divisors b1) <> 0 ;
then len G <> 0 by ;
then A5: not G is empty ;
then A6: 1 in dom G by FINSEQ_5:6;
then reconsider G1 = G . 1 as Element of (Bags (o1 +^ o2)) * by ;
G = <*(G . 1)*> ^ (Del (G,1)) by ;
then A7: FlattenSeq G = () ^ () by PRE_POLY:3
.= G1 ^ () by PRE_POLY:1 ;
set F = FlattenSeq G;
A8: for n, m being Nat st n in dom () & m in dom () & n < m holds
( () /. n <> () /. m & [(() /. n),(() /. m)] in BagOrder (o1 +^ o2) )
proof
let n, m be Nat; :: thesis: ( n in dom () & m in dom () & n < m implies ( () /. n <> () /. m & [(() /. n),(() /. m)] in BagOrder (o1 +^ o2) ) )
assume that
A9: n in dom () and
A10: m in dom () and
A11: n < m ; :: thesis: ( () /. n <> () /. m & [(() /. n),(() /. m)] in BagOrder (o1 +^ o2) )
A12: (FlattenSeq G) /. n = () . n by ;
consider i1, j1 being Nat such that
A13: i1 in dom G and
A14: j1 in dom (G . i1) and
A15: n = (Sum (Card (G | (i1 -' 1)))) + j1 and
A16: (G . i1) . j1 = () . n by ;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A17: Fk = G /. i1 and
A18: (divisors b1) /. i1 = a19 and
A19: len Fk = len (divisors b2) and
A20: for r being Nat st r in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. r = a199 & Fk /. r = a19 +^ a199 ) by A1, A2, A13;
A21: j1 in dom Fk by ;
then consider a199 being Element of Bags o2 such that
A22: (divisors b2) /. j1 = a199 and
A23: Fk /. j1 = a19 +^ a199 by A20;
Seg (len Fk) = dom Fk by FINSEQ_1:def 3;
then A24: j1 in dom (divisors b2) by ;
now :: thesis: not () /. n = () /. m
consider i2, j2 being Nat such that
A25: i2 in dom G and
A26: j2 in dom (G . i2) and
A27: m = (Sum (Card (G | (i2 -' 1)))) + j2 and
A28: (G . i2) . j2 = () . m by ;
consider a29 being Element of Bags o1, Fk9 being FinSequence of Bags (o1 +^ o2) such that
A29: Fk9 = G /. i2 and
A30: (divisors b1) /. i2 = a29 and
A31: len Fk9 = len (divisors b2) and
A32: for r being Nat st r in dom Fk9 holds
ex a299 being Element of Bags o2 st
( (divisors b2) /. r = a299 & Fk9 /. r = a29 +^ a299 ) by A1, A2, A25;
A33: (divisors b1) . i2 = a29 by ;
Fk9 = G . i2 by ;
then A34: (FlattenSeq G) . m = Fk9 /. j2 by ;
A35: j2 in dom Fk9 by ;
then consider a299 being Element of Bags o2 such that
A36: (divisors b2) /. j2 = a299 and
A37: Fk9 /. j2 = a29 +^ a299 by A32;
Seg (len Fk9) = dom Fk9 by FINSEQ_1:def 3;
then A38: j2 in dom (divisors b2) by ;
then A39: (divisors b2) . j2 = a299 by ;
consider i1, j1 being Nat such that
A40: i1 in dom G and
A41: j1 in dom (G . i1) and
A42: n = (Sum (Card (G | (i1 -' 1)))) + j1 and
A43: (G . i1) . j1 = () . n by ;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A44: Fk = G /. i1 and
A45: (divisors b1) /. i1 = a19 and
A46: len Fk = len (divisors b2) and
A47: for r being Nat st r in dom Fk holds
ex a199 being Element of Bags o2 st
( (divisors b2) /. r = a199 & Fk /. r = a19 +^ a199 ) by A1, A2, A40;
A48: (divisors b1) . i1 = a19 by ;
Fk = G . i1 by ;
then A49: (FlattenSeq G) . n = Fk /. j1 by ;
A50: j1 in dom Fk by ;
then consider a199 being Element of Bags o2 such that
A51: (divisors b2) /. j1 = a199 and
A52: Fk /. j1 = a19 +^ a199 by A47;
Seg (len Fk) = dom Fk by FINSEQ_1:def 3;
then A53: j1 in dom (divisors b2) by ;
then A54: (divisors b2) . j1 = a199 by ;
assume A55: (FlattenSeq G) /. n = () /. m ; :: thesis: contradiction
A56: ( (FlattenSeq G) /. n = () . n & () /. m = () . m ) by ;
then a19 = a29 by A55, A52, A37, A49, A34, Th7;
then A57: i1 = i2 by ;
a199 = a299 by A55, A56, A52, A37, A49, A34, Th7;
hence contradiction by A11, A42, A27, A57, A53, A54, A38, A39, FUNCT_1:def 4; :: thesis: verum
end;
hence (FlattenSeq G) /. n <> () /. m ; :: thesis: [(() /. n),(() /. m)] in BagOrder (o1 +^ o2)
reconsider Fn = () /. n, Fm = () /. m as bag of o1 +^ o2 ;
reconsider Fn9 = Fn, Fm9 = Fm as Element of Bags (o1 +^ o2) ;
consider a1 being Element of Bags o1, a2 being Element of Bags o2 such that
A58: Fn9 = a1 +^ a2 by Th6;
Fk = G . i1 by ;
then A59: Fn9 = Fk /. j1 by ;
then A60: a19 = a1 by ;
then A61: (divisors b1) . i1 = a1 by ;
A62: a199 = a2 by A58, A23, A59, Th7;
then A63: (divisors b2) . j1 = a2 by ;
A64: (FlattenSeq G) /. m = () . m by ;
consider c1 being Element of Bags o1, c2 being Element of Bags o2 such that
A65: Fm9 = c1 +^ c2 by Th6;
consider i2, j2 being Nat such that
A66: i2 in dom G and
A67: j2 in dom (G . i2) and
A68: m = (Sum (Card (G | (i2 -' 1)))) + j2 and
A69: (G . i2) . j2 = () . m by ;
consider a29 being Element of Bags o1, Fk9 being FinSequence of Bags (o1 +^ o2) such that
A70: Fk9 = G /. i2 and
A71: (divisors b1) /. i2 = a29 and
A72: len Fk9 = len (divisors b2) and
A73: for r being Nat st r in dom Fk9 holds
ex a299 being Element of Bags o2 st
( (divisors b2) /. r = a299 & Fk9 /. r = a29 +^ a299 ) by A1, A2, A66;
A74: j2 in dom Fk9 by ;
then consider a299 being Element of Bags o2 such that
A75: (divisors b2) /. j2 = a299 and
A76: Fk9 /. j2 = a29 +^ a299 by A73;
Seg (len Fk9) = dom Fk9 by FINSEQ_1:def 3;
then A77: j2 in dom (divisors b2) by ;
Fk9 = G . i2 by ;
then A78: Fm9 = Fk9 /. j2 by ;
then A79: a29 = c1 by ;
then A80: (divisors b1) . i2 = c1 by ;
A81: a299 = c2 by A65, A76, A78, Th7;
then A82: (divisors b2) . j2 = c2 by ;
now :: thesis: ( ( i1 < i2 & a1 < c1 ) or ( i1 = i2 & j1 < j2 & a1 = c1 & a2 < c2 ) )
A83: now :: thesis: ( not i1 < i2 implies ( i1 = i2 & j1 < j2 ) )
assume that
A84: not i1 < i2 and
A85: ( not i1 = i2 or not j1 < j2 ) ; :: thesis: contradiction
per cases ( i1 = i2 or i1 > i2 ) by ;
suppose A86: i1 > i2 ; :: thesis: contradiction
i2 >= 1 by ;
then A87: i2 -' 1 = i2 - 1 by XREAL_1:233;
reconsider G1 = G . i2 as Element of (Bags (o1 +^ o2)) * by ;
A88: ( Card (G | i2) = (Card G) | i2 & Card (G | (i1 -' 1)) = (Card G) | (i1 -' 1) ) by POLYNOM3:16;
reconsider GG1 = <*G1*> as FinSequence of (Bags (o1 +^ o2)) * ;
i2 < i2 + 1 by XREAL_1:29;
then A89: i2 - 1 < i2 by XREAL_1:19;
i2 >= 1 by ;
then A90: (i2 -' 1) + 1 = i2 by XREAL_1:235;
i2 <= len G by ;
then i2 -' 1 < len G by ;
then G | i2 = (G | (i2 -' 1)) ^ GG1 by ;
then Card (G | i2) = (Card (G | (i2 -' 1))) ^ (Card GG1) by PRE_POLY:25;
then Card (G | i2) = (Card (G | (i2 -' 1))) ^ <*(card G1)*> by PRE_POLY:24;
then A91: Sum (Card (G | i2)) = (Sum (Card (G | (i2 -' 1)))) + (card (G . i2)) by RVSUM_1:74;
j2 <= card (G . i2) by ;
then A92: (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | i2)) by ;
i2 <= i1 -' 1 by ;
then Sum (Card (G | i2)) <= Sum (Card (G | (i1 -' 1))) by ;
then A93: (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | (i1 -' 1))) by ;
Sum (Card (G | (i1 -' 1))) <= (Sum (Card (G | (i1 -' 1)))) + j1 by NAT_1:11;
hence contradiction by A11, A15, A68, A93, XXREAL_0:2; :: thesis: verum
end;
end;
end;
consider S being non empty finite Subset of (Bags o1) such that
A94: divisors b1 = SgmX ((BagOrder o1),S) and
for p being bag of o1 holds
( p in S iff p divides b1 ) by PRE_POLY:def 16;
field (BagOrder o1) = Bags o1 by ORDERS_1:15;
then A95: BagOrder o1 linearly_orders S by ;
consider T being non empty finite Subset of (Bags o2) such that
A96: divisors b2 = SgmX ((BagOrder o2),T) and
for p being bag of o2 holds
( p in T iff p divides b2 ) by PRE_POLY:def 16;
field (BagOrder o2) = Bags o2 by ORDERS_1:15;
then A97: BagOrder o2 linearly_orders T by ;
per cases ( i1 < i2 or ( i1 = i2 & j1 < j2 ) ) by A83;
case A98: i1 < i2 ; :: thesis: a1 < c1
then [((divisors b1) /. i1),((divisors b1) /. i2)] in BagOrder o1 by ;
then A99: a1 <=' c1 by ;
a1 <> c1 by ;
hence a1 < c1 by ; :: thesis: verum
end;
case that A100: i1 = i2 and
A101: j1 < j2 ; :: thesis: ( a1 = c1 & a2 < c2 )
[((divisors b2) /. j1),((divisors b2) /. j2)] in BagOrder o2 by ;
then A102: a2 <=' c2 by ;
thus a1 = c1 by A65, A18, A71, A76, A78, A60, A100, Th7; :: thesis: a2 < c2
a2 <> c2 by ;
hence a2 < c2 by ; :: thesis: verum
end;
end;
end;
then ( Fn < Fm or Fn = Fm ) by ;
then Fn <=' Fm by PRE_POLY:def 10;
hence [(() /. n),(() /. m)] in BagOrder (o1 +^ o2) by PRE_POLY:def 14; :: thesis: verum
end;
Fk = G . 1 by ;
then G . 1 <> {} by A4;
then reconsider S = rng () as non empty finite Subset of (Bags (o1 +^ o2)) by ;
A103: for p being bag of o1 +^ o2 holds
( p in S iff p divides b1 +^ b2 )
proof
consider W being non empty finite Subset of (Bags o2) such that
A104: divisors b2 = SgmX ((BagOrder o2),W) and
A105: for q being bag of o2 holds
( q in W iff q divides b2 ) by PRE_POLY:def 16;
field (BagOrder o2) = Bags o2 by ORDERS_1:15;
then BagOrder o2 linearly_orders W by ;
then A106: rng (SgmX ((BagOrder o2),W)) = W by PRE_POLY:def 2;
let p be bag of o1 +^ o2; :: thesis: ( p in S iff p divides b1 +^ b2 )
consider T being non empty finite Subset of (Bags o1) such that
A107: divisors b1 = SgmX ((BagOrder o1),T) and
A108: for q being bag of o1 holds
( q in T iff q divides b1 ) by PRE_POLY:def 16;
field (BagOrder o1) = Bags o1 by ORDERS_1:15;
then BagOrder o1 linearly_orders T by ;
then A109: rng (SgmX ((BagOrder o1),T)) = T by PRE_POLY:def 2;
thus ( p in S implies p divides b1 +^ b2 ) :: thesis: ( p divides b1 +^ b2 implies p in S )
proof
assume p in S ; :: thesis: p divides b1 +^ b2
then consider x being object such that
A110: x in dom () and
A111: p = () . x by FUNCT_1:def 3;
consider i, j being Nat such that
A112: i in dom G and
A113: j in dom (G . i) and
x = (Sum (Card (G | (i -' 1)))) + j and
A114: (G . i) . j = () . x by ;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A115: Fk = G /. i and
A116: (divisors b1) /. i = a19 and
A117: len Fk = len (divisors b2) and
A118: 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 ) by A1, A2, A112;
reconsider a119 = a19 as bag of o1 ;
(divisors b1) . i = a19 by ;
then a19 in T by ;
then A119: a119 divides b1 by A108;
A120: Fk = G . i by ;
then consider a199 being Element of Bags o2 such that
A121: (divisors b2) /. j = a199 and
A122: Fk /. j = a19 +^ a199 by ;
reconsider a1199 = a199 as bag of o2 ;
j in Seg (len Fk) by ;
then A123: j in dom (divisors b2) by ;
then (divisors b2) . j = a199 by ;
then a199 in W by ;
then A124: a1199 divides b2 by A105;
p = a19 +^ a199 by ;
hence p divides b1 +^ b2 by ; :: thesis: verum
end;
thus ( p divides b1 +^ b2 implies p in S ) :: thesis: verum
proof
assume p divides b1 +^ b2 ; :: thesis: p in S
then consider p1 being Element of Bags o1, p2 being Element of Bags o2 such that
A125: p1 divides b1 and
A126: p2 divides b2 and
A127: p = p1 +^ p2 by Th10;
p1 in T by ;
then consider i being object such that
A128: i in dom (divisors b1) and
A129: p1 = (divisors b1) . i by ;
reconsider i = i as Element of NAT by A128;
consider a19 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A130: Fk = G /. i and
A131: (divisors b1) /. i = a19 and
A132: len Fk = len (divisors b2) and
A133: 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 ) by ;
A134: a19 = p1 by ;
p2 in rng (divisors b2) by ;
then consider j being object such that
A135: j in dom (divisors b2) and
A136: p2 = (divisors b2) . j by FUNCT_1:def 3;
A137: j in Seg (len (divisors b2)) by ;
Seg (len (G . i)) = Seg (len (divisors b2)) by ;
then A138: j in dom (G . i) by ;
reconsider j = j as Element of NAT by A135;
A139: G /. i = G . i by ;
then consider a199 being Element of Bags o2 such that
A140: (divisors b2) /. j = a199 and
A141: Fk /. j = a19 +^ a199 by ;
A142: a199 = p2 by ;
A143: ( (Sum (Card (G | (i -' 1)))) + j in dom () & (G . i) . j = () . ((Sum (Card (G | (i -' 1)))) + j) ) by ;
(G . i) . j = a19 +^ a199 by ;
hence p in S by ; :: thesis: verum
end;
end;
field (BagOrder (o1 +^ o2)) = Bags (o1 +^ o2) by ORDERS_1:15;
then BagOrder (o1 +^ o2) linearly_orders S by ;
then FlattenSeq G = SgmX ((BagOrder (o1 +^ o2)),S) by ;
hence divisors (b1 +^ b2) = FlattenSeq G by ; :: thesis: verum