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 a1' being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = G /. i & (divisors b1) /. i = a1' & len Fk = len (divisors b2) & ( for m being Nat st m in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. m = a1'' & Fk /. m = a1' +^ a1'' ) ) ) ; :: thesis:
len (divisors b1) <> 0 ;
then len G <> 0 by A1, FINSEQ_3:31;
then A3: not G is empty ;
then A4: G = <*(G . 1)*> ^ (Del G,1) by POLYALG1:4;
reconsider D = Del G,1 as FinSequence of (Bags (o1 +^ o2)) * ;
A5: 1 in dom G by A3, FINSEQ_5:6;
then consider a1' being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A6: ( Fk = G /. 1 & (divisors b1) /. 1 = a1' ) and
A7: len Fk = len (divisors b2) and
for m being Nat st m in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. m = a1'' & Fk /. m = a1' +^ a1'' ) by A1, A2;
reconsider G1 = G . 1 as Element of (Bags (o1 +^ o2)) * by A5, A6, PARTFUN1:def 8;
A8: FlattenSeq G = (FlattenSeq <*G1*>) ^ (FlattenSeq D) by A4, DTCONSTR:21
.= G1 ^ (FlattenSeq D) by DTCONSTR:13 ;
A9: Fk = G . 1 by A5, A6, PARTFUN1:def 8;
G . 1 <> {} by A7, A9;
then FlattenSeq G <> {} by A8;
then reconsider S = rng (FlattenSeq G) as non empty finite Subset of (Bags (o1 +^ o2)) by FINSEQ_1:def 4, RELAT_1:64;
set F = FlattenSeq G;
field (BagOrder (o1 +^ o2)) = Bags (o1 +^ o2) by ORDERS_1:100;
then A10: BagOrder (o1 +^ o2) linearly_orders S by ORDERS_1:133, ORDERS_1:134;
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
A11: ( n in dom (FlattenSeq G) & m in dom (FlattenSeq G) ) and
A12: n < m ; :: thesis:

now

assume A13: (FlattenSeq G) /. n = (FlattenSeq G) /. m ; :: thesis:
A14: (FlattenSeq G) /. n = (FlattenSeq G) . n by A11, PARTFUN1:def 8;
A15: (FlattenSeq G) /. m = (FlattenSeq G) . m by A11, PARTFUN1:def 8;
consider i1, j1 being Element of NAT such that
A16: i1 in dom G and
A17: j1 in dom (G . i1) and
A18: n = (Sum (Card (G | (i1 -' 1)))) + j1 and
A19: (G . i1) . j1 = (FlattenSeq G) . n by A11, POLYNOM1:32;
consider i2, j2 being Element of NAT such that
A20: i2 in dom G and
A21: j2 in dom (G . i2) and
A22: m = (Sum (Card (G | (i2 -' 1)))) + j2 and
A23: (G . i2) . j2 = (FlattenSeq G) . m by A11, POLYNOM1:32;
consider a1' being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A24: Fk = G /. i1 and
A25: (divisors b1) /. i1 = a1' and
A26: len Fk = len (divisors b2) and
A27: for r being Nat st r in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. r = a1'' & Fk /. r = a1' +^ a1'' ) by A1, A2, A16;
A28: j1 in dom Fk by A16, A17, A24, PARTFUN1:def 8;
then consider a1'' being Element of Bags o2 such that
A29: (divisors b2) /. j1 = a1'' and
A30: Fk /. j1 = a1' +^ a1'' by A27;
consider a2' being Element of Bags o1, Fk' being FinSequence of Bags (o1 +^ o2) such that
A31: Fk' = G /. i2 and
A32: (divisors b1) /. i2 = a2' and
A33: len Fk' = len (divisors b2) and
A34: for r being Nat st r in dom Fk' holds
ex a2'' being Element of Bags o2 st
( (divisors b2) /. r = a2'' & Fk' /. r = a2' +^ a2'' ) by A1, A2, A20;
A35: j2 in dom Fk' by A20, A21, A31, PARTFUN1:def 8;
then consider a2'' being Element of Bags o2 such that
A36: (divisors b2) /. j2 = a2'' and
A37: Fk' /. j2 = a2' +^ a2'' by A34;
Fk = G . i1 by A16, A24, PARTFUN1:def 8;
then A38: (FlattenSeq G) . n = Fk /. j1 by A17, A19, PARTFUN1:def 8;
Fk' = G . i2 by A20, A31, PARTFUN1:def 8;
then (FlattenSeq G) . m = Fk' /. j2 by A21, A23, PARTFUN1:def 8;
then A39: ( a1' = a2' & a1'' = a2'' ) by A13, A14, A15, A30, A37, A38, Th7;
A40: (divisors b1) . i1 = a1' by A1, A16, A25, PARTFUN1:def 8;
(divisors b1) . i2 = a2' by A1, A20, A32, PARTFUN1:def 8;
then A41: i1 = i2 by A1, A16, A20, A39, A40, FUNCT_1:def 8;
Seg (len Fk) = dom Fk by FINSEQ_1:def 3;
then A42: j1 in dom (divisors b2) by A26, A28, FINSEQ_1:def 3;
then A43: (divisors b2) . j1 = a1'' by A29, PARTFUN1:def 8;
Seg (len Fk') = dom Fk' by FINSEQ_1:def 3;
then A44: j2 in dom (divisors b2) by A33, A35, FINSEQ_1:def 3;
then (divisors b2) . j2 = a2'' by A36, PARTFUN1:def 8;
hence contradiction by A12, A18, A22, A39, A41, A42, A43, A44, FUNCT_1:def 8; :: thesis:

end;

hence (FlattenSeq G) /. n <> (FlattenSeq G) /. m ; :: thesis:
A45: (FlattenSeq G) /. n = (FlattenSeq G) . n by A11, PARTFUN1:def 8;
A46: (FlattenSeq G) /. m = (FlattenSeq G) . m by A11, PARTFUN1:def 8;
reconsider Fn = (FlattenSeq G) /. n, Fm = (FlattenSeq G) /. m as bag of by POLYNOM1:def 14;
reconsider Fn' = Fn, Fm' = Fm as Element of Bags (o1 +^ o2) ;
consider a1 being Element of Bags o1, a2 being Element of Bags o2 such that
A47: Fn' = a1 +^ a2 by Th6;
consider c1 being Element of Bags o1, c2 being Element of Bags o2 such that
A48: Fm' = c1 +^ c2 by Th6;
consider i1, j1 being Element of NAT such that
A49: i1 in dom G and
A50: j1 in dom (G . i1) and
A51: n = (Sum (Card (G | (i1 -' 1)))) + j1 and
A52: (G . i1) . j1 = (FlattenSeq G) . n by A11, POLYNOM1:32;
consider i2, j2 being Element of NAT such that
A53: i2 in dom G and
A54: j2 in dom (G . i2) and
A55: m = (Sum (Card (G | (i2 -' 1)))) + j2 and
A56: (G . i2) . j2 = (FlattenSeq G) . m by A11, POLYNOM1:32;
consider a1' being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A57: Fk = G /. i1 and
A58: (divisors b1) /. i1 = a1' and
A59: len Fk = len (divisors b2) and
A60: for r being Nat st r in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. r = a1'' & Fk /. r = a1' +^ a1'' ) by A1, A2, A49;
A61: j1 in dom Fk by A49, A50, A57, PARTFUN1:def 8;
then consider a1'' being Element of Bags o2 such that
A62: (divisors b2) /. j1 = a1'' and
A63: Fk /. j1 = a1' +^ a1'' by A60;
consider a2' being Element of Bags o1, Fk' being FinSequence of Bags (o1 +^ o2) such that
A64: Fk' = G /. i2 and
A65: (divisors b1) /. i2 = a2' and
A66: len Fk' = len (divisors b2) and
A67: for r being Nat st r in dom Fk' holds
ex a2'' being Element of Bags o2 st
( (divisors b2) /. r = a2'' & Fk' /. r = a2' +^ a2'' ) by A1, A2, A53;
A68: j2 in dom Fk' by A53, A54, A64, PARTFUN1:def 8;
then consider a2'' being Element of Bags o2 such that
A69: (divisors b2) /. j2 = a2'' and
A70: Fk' /. j2 = a2' +^ a2'' by A67;
Fk = G . i1 by A49, A57, PARTFUN1:def 8;
then A71: Fn' = Fk /. j1 by A45, A50, A52, PARTFUN1:def 8;
Fk' = G . i2 by A53, A64, PARTFUN1:def 8;
then Fm' = Fk' /. j2 by A46, A54, A56, PARTFUN1:def 8;
then A72: ( a1' = a1 & a1'' = a2 & a2' = c1 & a2'' = c2 ) by A47, A48, A63, A70, A71, Th7;
then A73: (divisors b1) . i1 = a1 by A1, A49, A58, PARTFUN1:def 8;
A74: (divisors b1) . i2 = c1 by A1, A53, A65, A72, PARTFUN1:def 8;
Seg (len Fk) = dom Fk by FINSEQ_1:def 3;
then A75: j1 in dom (divisors b2) by A59, A61, FINSEQ_1:def 3;
then A76: (divisors b2) . j1 = a2 by A62, A72, PARTFUN1:def 8;
Seg (len Fk') = dom Fk' by FINSEQ_1:def 3;
then A77: j2 in dom (divisors b2) by A66, A68, FINSEQ_1:def 3;
then A78: (divisors b2) . j2 = c2 by A69, A72, PARTFUN1:def 8;

now

consider S being non empty finite Subset of (Bags o1) such that
A79: divisors b1 = SgmX (BagOrder o1),S and
for p being bag of holds
( p in S iff p divides b1 ) by POLYNOM1:def 18;
field (BagOrder o1) = Bags o1 by ORDERS_1:100;
then A80: BagOrder o1 linearly_orders S by ORDERS_1:133, ORDERS_1:134;
consider T being non empty finite Subset of (Bags o2) such that
A81: divisors b2 = SgmX (BagOrder o2),T and
for p being bag of holds
( p in T iff p divides b2 ) by POLYNOM1:def 18;
field (BagOrder o2) = Bags o2 by ORDERS_1:100;
then A82: BagOrder o2 linearly_orders T by ORDERS_1:133, ORDERS_1:134;

A83: now

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 A12, A51, A55, A85, XREAL_1:8; :: thesis:

end;

suppose A86: i1 > i2 ; :: thesis:

A87: j2 <= card (G . i2) by A54, FINSEQ_3:27;
A88: Card (G | i2) = (Card G) | i2 by POLYNOM3:16;
A89: Card (G | (i1 -' 1)) = (Card G) | (i1 -' 1) by POLYNOM3:16;
i2 <= i1 -' 1 by A86, NAT_D:49;
then A90: Sum (Card (G | i2)) <= Sum (Card (G | (i1 -' 1))) by A88, A89, POLYNOM3:18;
i2 >= 1 by A53, FINSEQ_3:27;
then A91: i2 -' 1 = i2 - 1 by XREAL_1:235;
i2 < i2 + 1 by XREAL_1:31;
then A92: i2 - 1 < i2 by XREAL_1:21;
i2 <= len G by A53, FINSEQ_3:27;
then A93: i2 -' 1 < len G by A91, A92, XXREAL_0:2;
i2 >= 1 by A53, FINSEQ_3:27;
then A94: (i2 -' 1) + 1 = i2 by XREAL_1:237;
reconsider G1 = G . i2 as Element of (Bags (o1 +^ o2)) * by A53, A64, PARTFUN1:def 8;
reconsider GG1 = <*G1*> as FinSequence of (Bags (o1 +^ o2)) * ;
G | i2 = (G | (i2 -' 1)) ^ GG1 by A93, A94, POLYNOM3:19;
then Card (G | i2) = (Card (G | (i2 -' 1))) ^ (Card GG1) by POLYNOM1:13;
then Card (G | i2) = (Card (G | (i2 -' 1))) ^ <*(card G1)*> by POLYNOM1:12;
then Sum (Card (G | i2)) = (Sum (Card (G | (i2 -' 1)))) + (card (G . i2)) by RVSUM_1:104;
then (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | i2)) by A87, XREAL_1:8;
then A95: (Sum (Card (G | (i2 -' 1)))) + j2 <= Sum (Card (G | (i1 -' 1))) by A90, XXREAL_0:2;
Sum (Card (G | (i1 -' 1))) <= (Sum (Card (G | (i1 -' 1)))) + j1 by NAT_1:11;
hence contradiction by A12, A51, A55, A95, XXREAL_0:2; :: thesis:

end;

per cases by A83;

case A96: i1 < i2 ; :: thesis:

then A97: [((divisors b1) /. i1),((divisors b1) /. i2)] in BagOrder o1 by A1, A49, A53, A79, A80, TRIANG_1:def 2;
A98: a1 <> c1 by A1, A49, A53, A73, A74, A96, FUNCT_1:def 8;
a1 <=' c1 by A58, A65, A72, A97, POLYNOM1:def 16;
hence a1 < c1 by A98, POLYNOM1:def 12; :: thesis:

end;

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

A101: [((divisors b2) /. j1),((divisors b2) /. j2)] in BagOrder o2 by A75, A77, A81, A82, A100, TRIANG_1:def 2;
thus a1 = c1 by A58, A65, A72, A99; :: thesis:
A102: a2 <> c2 by A75, A76, A77, A78, A100, FUNCT_1:def 8;
a2 <=' c2 by A62, A69, A72, A101, POLYNOM1:def 16;
hence a2 < c2 by A102, POLYNOM1:def 12; :: thesis:

end;

then ( Fn < Fm or Fn = Fm ) by A47, A48, Th11;
then Fn <=' Fm by POLYNOM1:def 12;
hence [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) by POLYNOM1:def 16; :: thesis:

end;

then A103: FlattenSeq G = SgmX (BagOrder (o1 +^ o2)),S by A10, TRIANG_1:def 2;
for p being bag of holds
( p in S iff p divides b1 +^ b2 )

proof

consider T being non empty finite Subset of (Bags o1) such that
A104: divisors b1 = SgmX (BagOrder o1),T and
A105: for q being bag of holds
( q in T iff q divides b1 ) by POLYNOM1:def 18;
consider W being non empty finite Subset of (Bags o2) such that
A106: divisors b2 = SgmX (BagOrder o2),W and
A107: for q being bag of holds
( q in W iff q divides b2 ) by POLYNOM1:def 18;
field (BagOrder o1) = Bags o1 by ORDERS_1:100;
then BagOrder o1 linearly_orders T by ORDERS_1:133, ORDERS_1:134;
then A108: rng (SgmX (BagOrder o1),T) = T by TRIANG_1:def 2;
field (BagOrder o2) = Bags o2 by ORDERS_1:100;
then BagOrder o2 linearly_orders W by ORDERS_1:133, ORDERS_1:134;
then A109: rng (SgmX (BagOrder o2),W) = W by TRIANG_1:def 2;
let p be bag of ; :: thesis:
thus ( p in S implies p divides b1 +^ b2 ) :: thesis:

proof

assume p in S ; :: thesis:
then consider x being set such that
A110: x in dom (FlattenSeq G) and
A111: p = (FlattenSeq G) . x by FUNCT_1:def 5;
consider i, j being Element of 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, POLYNOM1:32;
consider a1' being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A115: Fk = G /. i and
A116: (divisors b1) /. i = a1' and
A117: len Fk = len (divisors b2) and
A118: for m being Nat st m in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. m = a1'' & Fk /. m = a1' +^ a1'' ) by A1, A2, A112;
A119: Fk = G . i by A112, A115, PARTFUN1:def 8;
then consider a1'' being Element of Bags o2 such that
A120: (divisors b2) /. j = a1'' and
A121: Fk /. j = a1' +^ a1'' by A113, A118;
A122: p = a1' +^ a1'' by A111, A113, A114, A119, A121, PARTFUN1:def 8;
(divisors b1) . i = a1' by A1, A112, A116, PARTFUN1:def 8;
then A123: a1' in T by A1, A104, A108, A112, FUNCT_1:12;
reconsider a11' = a1' as bag of ;
A124: a11' divides b1 by A105, A123;
j in Seg (len Fk) by A113, A119, FINSEQ_1:def 3;
then A125: j in dom (divisors b2) by A117, FINSEQ_1:def 3;
then (divisors b2) . j = a1'' by A120, PARTFUN1:def 8;
then A126: a1'' in W by A106, A109, A125, FUNCT_1:12;
reconsider a11'' = a1'' as bag of ;
a11'' divides b2 by A107, A126;
hence p divides b1 +^ b2 by A122, 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
A127: p1 divides b1 and
A128: p2 divides b2 and
A129: p = p1 +^ p2 by Th10;
p1 in T by A105, A127;
then consider i being set such that
A130: i in dom (divisors b1) and
A131: p1 = (divisors b1) . i by A104, A108, FUNCT_1:def 5;
p2 in rng (divisors b2) by A106, A107, A109, A128;
then consider j being set such that
A132: j in dom (divisors b2) and
A133: p2 = (divisors b2) . j by FUNCT_1:def 5;
reconsider i = i as Element of NAT by A130;
consider a1' being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A134: Fk = G /. i and
A135: (divisors b1) /. i = a1' and
A136: len Fk = len (divisors b2) and
A137: for m being Nat st m in dom Fk holds
ex a1'' being Element of Bags o2 st
( (divisors b2) /. m = a1'' & Fk /. m = a1' +^ a1'' ) by A2, A130;
A138: j in Seg (len (divisors b2)) by A132, FINSEQ_1:def 3;
Seg (len (G . i)) = Seg (len (divisors b2)) by A1, A130, A134, A136, PARTFUN1:def 8;
then A139: j in dom (G . i) by A138, FINSEQ_1:def 3;
reconsider j = j as Element of NAT by A132;
A140: ( (Sum (Card (G | (i -' 1)))) + j in dom (FlattenSeq G) & (G . i) . j = (FlattenSeq G) . ((Sum (Card (G | (i -' 1)))) + j) ) by A1, A130, A139, POLYNOM1:33;
A141: G /. i = G . i by A1, A130, PARTFUN1:def 8;
then consider a1'' being Element of Bags o2 such that
A142: (divisors b2) /. j = a1'' and
A143: Fk /. j = a1' +^ a1'' by A134, A137, A139;
A144: (G . i) . j = a1' +^ a1'' by A134, A139, A141, A143, PARTFUN1:def 8;
A145: a1' = p1 by A130, A131, A135, PARTFUN1:def 8;
a1'' = p2 by A132, A133, A142, PARTFUN1:def 8;
hence p in S by A129, A140, A144, A145, FUNCT_1:def 5; :: thesis:

end;

hence divisors (b1 +^ b2) = FlattenSeq G by A103, POLYNOM1:def 18; :: thesis: