let o1, o2 be 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
let b1 be 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 b2 be 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 G be FinSequence of (Bags (o1 +^ o2)) * ; ( 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 ) ) )
; 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 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;
( n in dom (FlattenSeq G) & m in dom (FlattenSeq G) & n < m implies ( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) ) )
assume that A9:
n in dom (FlattenSeq G)
and A10:
m in dom (FlattenSeq G)
and A11:
n < m
;
( (FlattenSeq G) /. n <> (FlattenSeq G) /. m & [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2) )
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 not (FlattenSeq G) /. n = (FlattenSeq G) /. mconsider 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
;
contradictionA56:
(
(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;
verum end;
hence
(FlattenSeq G) /. n <> (FlattenSeq G) /. m
;
[((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2)
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 ( ( i1 < i2 & a1 < c1 ) or ( i1 = i2 & j1 < j2 & a1 = c1 & a2 < c2 ) )A83:
now ( not i1 < i2 implies ( i1 = i2 & j1 < j2 ) )assume that A84:
not
i1 < i2
and A85:
( not
i1 = i2 or not
j1 < j2 )
;
contradictionper cases
( i1 = i2 or i1 > i2 )
by A84, XXREAL_0:1;
suppose A86:
i1 > i2
;
contradiction
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;
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 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
( i1 < i2 or ( i1 = i2 & j1 < j2 ) )
by A83;
case A98:
i1 < i2
;
a1 < c1then
[((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;
verum end; case that A100:
i1 = i2
and A101:
j1 < j2
;
( a1 = c1 & a2 < c2 )
[((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;
a2 < c2
a2 <> c2
by A24, A63, A77, A82, A101, FUNCT_1:def 4;
hence
a2 < c2
by A102, PRE_POLY:def 10;
verum end; end; 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;
verum
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;
( 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 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 )
( p divides b1 +^ b2 implies p in S )proof
assume
p in S
;
p divides b1 +^ b2
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;
verum
end;
thus
(
p divides b1 +^ b2 implies
p in S )
verumproof
assume
p divides b1 +^ b2
;
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 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;
verum
end;
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; verum