let o1, o2 be Ordinal; :: thesis:
let b1 be Element of Bags o1; :: thesis:
let b2 be Element of Bags o2; :: thesis:
let G be FinSequence of (Bags (o1 +^ o2)) * ; :: thesis:
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:
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 A2, FINSEQ_5:6;
len (divisors b1) <> 0 ;
then len G <> 0 by A1, FINSEQ_3:29;
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 A3, PARTFUN1:def 6;
G = <*(G . 1)*> ^ (Del (G,1)) by A5, FINSEQ_5:86;
then A7: FlattenSeq G = (FlattenSeq <*G1*>) ^ (FlattenSeq D) by PRE_POLY:3
.= G1 ^ (FlattenSeq D) by PRE_POLY:1 ;
set F = FlattenSeq G;
A8: for n, m being Nat st n in dom (FlattenSeq G) & m in dom (FlattenSeq G) & n < m holds
( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) )

proof

let n, m be Nat; :: thesis:
assume that
A9: n in dom (FlattenSeq G) and
A10: m in dom (FlattenSeq G) and
A11: n < m ; :: thesis:
A12: (FlattenSeq G) /. n = (FlattenSeq G) . n by A9, PARTFUN1:def 6;
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 = (FlattenSeq G) . n by A9, PRE_POLY:29;
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 A13, A14, A17, PARTFUN1:def 6;
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 A19, A21, FINSEQ_1:def 3;

now :: thesis:

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 = (FlattenSeq G) . m by A10, PRE_POLY:29;
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 A1, A25, A30, PARTFUN1:def 6;
Fk9 = G . i2 by A25, A29, PARTFUN1:def 6;
then A34: (FlattenSeq G) . m = Fk9 /. j2 by A26, A28, PARTFUN1:def 6;
A35: j2 in dom Fk9 by A25, A26, A29, PARTFUN1:def 6;
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 A31, A35, FINSEQ_1:def 3;
then A39: (divisors b2) . j2 = a299 by A36, PARTFUN1:def 6;
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 = (FlattenSeq G) . n by A9, PRE_POLY:29;
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 A1, A40, A45, PARTFUN1:def 6;
Fk = G . i1 by A40, A44, PARTFUN1:def 6;
then A49: (FlattenSeq G) . n = Fk /. j1 by A41, A43, PARTFUN1:def 6;
A50: j1 in dom Fk by A40, A41, A44, PARTFUN1:def 6;
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 A46, A50, FINSEQ_1:def 3;
then A54: (divisors b2) . j1 = a199 by A51, PARTFUN1:def 6;
assume A55: (FlattenSeq G) /. n = (FlattenSeq G) /. m ; :: thesis:
A56: ( (FlattenSeq G) /. n = (FlattenSeq G) . n & (FlattenSeq G) /. m = (FlattenSeq G) . m ) by A9, A10, PARTFUN1:def 6;
then a19 = a29 by A55, A52, A37, A49, A34, Th7;
then A57: i1 = i2 by A1, A40, A25, A48, A33, FUNCT_1:def 4;
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:

end;

hence (FlattenSeq G) /. n <> (FlattenSeq G) /. m ; :: thesis:
reconsider Fn = (FlattenSeq G) /. n, Fm = (FlattenSeq G) /. 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 A13, A17, PARTFUN1:def 6;
then A59: Fn9 = Fk /. j1 by A12, A14, A16, PARTFUN1:def 6;
then A60: a19 = a1 by A58, A23, Th7;
then A61: (divisors b1) . i1 = a1 by A1, A13, A18, PARTFUN1:def 6;
A62: a199 = a2 by A58, A23, A59, Th7;
then A63: (divisors b2) . j1 = a2 by A22, A24, PARTFUN1:def 6;
A64: (FlattenSeq G) /. m = (FlattenSeq G) . m by A10, PARTFUN1:def 6;
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 = (FlattenSeq G) . m by A10, PRE_POLY:29;
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 A66, A67, A70, PARTFUN1:def 6;
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 A72, A74, FINSEQ_1:def 3;
Fk9 = G . i2 by A66, A70, PARTFUN1:def 6;
then A78: Fm9 = Fk9 /. j2 by A64, A67, A69, PARTFUN1:def 6;
then A79: a29 = c1 by A65, A76, Th7;
then A80: (divisors b1) . i2 = c1 by A1, A66, A71, PARTFUN1:def 6;
A81: a299 = c2 by A65, A76, A78, Th7;
then A82: (divisors b2) . j2 = c2 by A75, A77, PARTFUN1:def 6;

now :: thesis:

A83: now :: thesis:

assume that
A84: not i1 < i2 and
A85: ( not i1 = i2 or not j1 < j2 ) ; :: thesis:

per cases by A84, XXREAL_0:1;

suppose i1 = i2 ; :: thesis:

hence contradiction by A11, A15, A68, A85, XREAL_1:6; :: thesis:

end;

suppose A86: i1 > i2 ; :: thesis:

i2 >= 1 by A66, FINSEQ_3:25;
then A87: i2 -' 1 = i2 - 1 by XREAL_1:233;
reconsider G1 = G . i2 as Element of (Bags (o1 +^ o2)) * by A66, A70, PARTFUN1:def 6;
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 A66, FINSEQ_3:25;
then A90: (i2 -' 1) + 1 = i2 by XREAL_1:235;
i2 <= len G by A66, FINSEQ_3:25;
then i2 -' 1 < len G by A87, A89, XXREAL_0:2;
then G | i2 = (G | (i2 -' 1)) ^ GG1 by A90, FINSEQ_5:83;
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 A67, FINSEQ_3:25;
then A92: (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | i2)) by A91, XREAL_1:6;
i2 <= i1 -' 1 by A86, NAT_D:49;
then Sum (Card (G | i2)) <= Sum (Card (G | (i1 -' 1))) by A88, POLYNOM3:18;
then A93: (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | (i1 -' 1))) by A92, XXREAL_0:2;
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:

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 ORDERS_1:37, ORDERS_1:38;
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 ORDERS_1:37, ORDERS_1:38;

per cases by A83;

case A98: i1 < i2 ; :: thesis:

then [((divisors b1) /. i1),((divisors b1) /. i2)] in BagOrder o1 by A1, A13, A66, A94, A95, PRE_POLY:def 2;
then A99: a1 <=' c1 by A18, A71, A60, A79, PRE_POLY:def 14;
a1 <> c1 by A1, A13, A66, A61, A80, A98, FUNCT_1:def 4;
hence a1 < c1 by A99, PRE_POLY:def 10; :: thesis:

end;

case that A100: i1 = i2 and
A101: j1 < j2 ; :: thesis:

[((divisors b2) /. j1),((divisors b2) /. j2)] in BagOrder o2 by A24, A77, A96, A97, A101, PRE_POLY:def 2;
then A102: a2 <=' c2 by A22, A75, A62, A81, PRE_POLY:def 14;
thus a1 = c1 by A65, A18, A71, A76, A78, A60, A100, Th7; :: thesis:
a2 <> c2 by A24, A63, A77, A82, A101, FUNCT_1:def 4;
hence a2 < c2 by A102, PRE_POLY:def 10; :: thesis:

end;

then ( Fn < Fm or Fn = Fm ) by A58, A65, Th11;
then Fn <=' Fm by PRE_POLY:def 10;
hence [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) by PRE_POLY:def 14; :: thesis:

end;

Fk = G . 1 by A6, A3, PARTFUN1:def 6;
then G . 1 <> {} by A4;
then reconsider S = rng (FlattenSeq G) as non empty finite Subset of (Bags (o1 +^ o2)) by A7, FINSEQ_1:def 4, RELAT_1:41;
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 ORDERS_1:37, ORDERS_1:38;
then A106: rng (SgmX ((BagOrder o2),W)) = W by PRE_POLY:def 2;
let p be bag of o1 +^ o2; :: thesis:
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 ORDERS_1:37, ORDERS_1:38;
then A109: rng (SgmX ((BagOrder o1),T)) = T by PRE_POLY:def 2;
thus ( p in S implies p divides b1 +^ b2 ) :: thesis:

proof

assume p in S ; :: thesis:
then consider x being object such that
A110: x in dom (FlattenSeq G) and
A111: p = (FlattenSeq G) . 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 = (FlattenSeq G) . x by A110, PRE_POLY:29;
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 A1, A112, A116, PARTFUN1:def 6;
then a19 in T by A1, A107, A109, A112, FUNCT_1:3;
then A119: a119 divides b1 by A108;
A120: Fk = G . i by A112, A115, PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A121: (divisors b2) /. j = a199 and
A122: Fk /. j = a19 +^ a199 by A113, A118;
reconsider a1199 = a199 as bag of o2 ;
j in Seg (len Fk) by A113, A120, FINSEQ_1:def 3;
then A123: j in dom (divisors b2) by A117, FINSEQ_1:def 3;
then (divisors b2) . j = a199 by A121, PARTFUN1:def 6;
then a199 in W by A104, A106, A123, FUNCT_1:3;
then A124: a1199 divides b2 by A105;
p = a19 +^ a199 by A111, A113, A114, A120, A122, PARTFUN1:def 6;
hence p divides b1 +^ b2 by A119, A124, Th9; :: thesis:

end;

thus ( p divides b1 +^ b2 implies p in S ) :: thesis:

proof

assume p divides b1 +^ b2 ; :: thesis:
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 A108, A125;
then consider i being object such that
A128: i in dom (divisors b1) and
A129: p1 = (divisors b1) . i by A107, A109, FUNCT_1:def 3;
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 A2, A128;
A134: a19 = p1 by A128, A129, A131, PARTFUN1:def 6;
p2 in rng (divisors b2) by A104, A105, A106, A126;
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 A135, FINSEQ_1:def 3;
Seg (len (G . i)) = Seg (len (divisors b2)) by A1, A128, A130, A132, PARTFUN1:def 6;
then A138: j in dom (G . i) by A137, FINSEQ_1:def 3;
reconsider j = j as Element of NAT by A135;
A139: G /. i = G . i by A1, A128, PARTFUN1:def 6;
then consider a199 being Element of Bags o2 such that
A140: (divisors b2) /. j = a199 and
A141: Fk /. j = a19 +^ a199 by A130, A133, A138;
A142: a199 = p2 by A135, A136, A140, PARTFUN1:def 6;
A143: ( (Sum (Card (G | (i -' 1)))) + j in dom (FlattenSeq G) & (G . i) . j = (FlattenSeq G) . ((Sum (Card (G | (i -' 1)))) + j) ) by A1, A128, A138, PRE_POLY:30;
(G . i) . j = a19 +^ a199 by A130, A138, A139, A141, PARTFUN1:def 6;
hence p in S by A127, A143, A134, A142, FUNCT_1:def 3; :: thesis:

end;

field (BagOrder (o1 +^ o2)) = Bags (o1 +^ o2) by ORDERS_1:15;
then BagOrder (o1 +^ o2) linearly_orders S by ORDERS_1:37, ORDERS_1:38;
then FlattenSeq G = SgmX ((BagOrder (o1 +^ o2)),S) by A8, PRE_POLY:def 2;
hence divisors (b1 +^ b2) = FlattenSeq G by A103, PRE_POLY:def 16; :: thesis: