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 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) )

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 )

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: verum

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 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

Fk = G . 1
by A6, A3, PARTFUN1:def 6;
let n, m be Nat; :: thesis: ( 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 ; :: thesis: ( (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;

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;

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: verum

end;assume that

A9: n in dom (FlattenSeq G) and

A10: m in dom (FlattenSeq G) and

A11: n < m ; :: thesis: ( (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 :: thesis: not (FlattenSeq G) /. n = (FlattenSeq G) /. m

hence
(FlattenSeq G) /. n <> (FlattenSeq G) /. m
; :: thesis: [((FlattenSeq G) /. n),((FlattenSeq G) /. m)] in BagOrder (o1 +^ o2)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: contradiction

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: verum

end;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: contradiction

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: verum

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: ( ( i1 < i2 & a1 < c1 ) or ( i1 = i2 & j1 < j2 & a1 = c1 & a2 < c2 ) )

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;

end;

then
( Fn < Fm or Fn = Fm )
by A58, A65, Th11;A83: now :: thesis: ( not i1 < i2 implies ( i1 = i2 & j1 < j2 ) )

consider S being non empty finite Subset of (Bags o1) such that assume that

A84: not i1 < i2 and

A85: ( not i1 = i2 or not j1 < j2 ) ; :: thesis: contradiction

end;A84: not i1 < i2 and

A85: ( not i1 = i2 or not j1 < j2 ) ; :: thesis: contradiction

per cases
( i1 = i2 or i1 > i2 )
by A84, XXREAL_0:1;

end;

suppose A86:
i1 > i2
; :: thesis: 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; :: thesis: verum

end;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: verum

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;

end;

case A98:
i1 < i2
; :: thesis: a1 < c1

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: verum

end;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: verum

case that A100:
i1 = i2
and

A101: j1 < j2 ; :: thesis: ( a1 = c1 & a2 < c2 )

A101: j1 < j2 ; :: thesis: ( 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; :: thesis: a2 < c2

a2 <> c2 by A24, A63, A77, A82, A101, FUNCT_1:def 4;

hence a2 < c2 by A102, PRE_POLY:def 10; :: thesis: verum

end;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

a2 <> c2 by A24, A63, A77, A82, A101, FUNCT_1:def 4;

hence a2 < c2 by A102, PRE_POLY:def 10; :: thesis: verum

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: verum

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

field (BagOrder (o1 +^ o2)) = Bags (o1 +^ o2)
by ORDERS_1:15;
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: ( 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 ) :: thesis: ( p divides b1 +^ b2 implies p in S )

end;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: ( 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 ) :: thesis: ( p divides b1 +^ b2 implies p in S )

proof

thus
( p divides b1 +^ b2 implies p in S )
:: thesis: verum
assume
p in S
; :: thesis: 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; :: thesis: verum

end;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: 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 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: verum

end;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: verum

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: verum