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 (2 -tuples_on (Bags (o1 +^ o2))) * ; :: thesis:
assume that
A1: dom G = dom (decomp b1) and
A2: for i being Nat st i in dom (decomp b1) holds
ex a1', b1' being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a1',b1'*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Fk /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) ) ) ; :: thesis:
defpred S₁[ set , Function] means ( dom $2 = dom (G . $1) & ( for j being Nat st j in dom $2 holds
ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . $1) . j & $2 . j = p . 1 ) ) );
A3: for k being Element of NAT st k in Seg (len G) holds
ex p being Element of (Bags (o1 +^ o2)) * st S₁[k,p]

proof

let k be Element of NAT ; :: thesis:
assume A4: k in Seg (len G) ; :: thesis:
defpred S₂[ set , set ] means ex q being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( q = (G . k) . $1 & $2 = q . 1 );
A5: for j being Element of NAT st j in Seg (len (G . k)) holds
ex x being Element of Bags (o1 +^ o2) st S₂[j,x]

proof

k in dom G by A4, FINSEQ_1:def 3;
then A6: G . k in rng G by FUNCT_1:12;
rng G c= (2 -tuples_on (Bags (o1 +^ o2))) * by FINSEQ_1:def 4;
then G . k is Element of (2 -tuples_on (Bags (o1 +^ o2))) * by A6;
then reconsider Gk = G . k as FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) ;
let j be Element of NAT ; :: thesis:
assume j in Seg (len (G . k)) ; :: thesis:
then j in dom (G . k) by FINSEQ_1:def 3;
then (G . k) . j = Gk /. j by PARTFUN1:def 8;
then reconsider q = (G . k) . j as Element of 2 -tuples_on (Bags (o1 +^ o2)) ;
ex q1, q2 being Element of Bags (o1 +^ o2) st q = <*q1,q2*> by FINSEQ_2:120;
then reconsider x = q . 1 as Element of Bags (o1 +^ o2) by FINSEQ_1:61;
take x ; :: thesis:
thus S₂[j,x] ; :: thesis:

end;

consider p being FinSequence of Bags (o1 +^ o2) such that
A7: dom p = Seg (len (G . k)) and
A8: for j being Element of NAT st j in Seg (len (G . k)) holds
S₂[j,p /. j] from POLYNOM2:sch 1(A5);
reconsider p = p as Element of (Bags (o1 +^ o2)) * by FINSEQ_1:def 11;
take p ; :: thesis:
thus dom p = dom (G . k) by A7, FINSEQ_1:def 3; :: thesis:
let j be Nat; :: thesis:
assume A9: j in dom p ; :: thesis:
then consider q being Element of 2 -tuples_on (Bags (o1 +^ o2)) such that
A10: q = (G . k) . j and
A11: p /. j = q . 1 by A7, A8;
take q ; :: thesis:
thus q = (G . k) . j by A10; :: thesis:
thus p . j = q . 1 by A9, A11, PARTFUN1:def 8; :: thesis:

end;

consider F being FinSequence of (Bags (o1 +^ o2)) * such that
A12: dom F = Seg (len G) and
A13: for i being Element of NAT st i in Seg (len G) holds
S₁[i,F /. i] from POLYNOM2:sch 1(A3);
A14: dom (Card F) = dom F by CARD_3:def 2
.= dom G by A12, FINSEQ_1:def 3
.= dom (Card G) by CARD_3:def 2 ;
A15: dom (divisors b1) = dom (decomp b1) by PRE_POLY:def 17;
A16: 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 = F /. 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'' ) ) )

proof

let i be Nat; :: thesis:
reconsider Fk = F /. i as FinSequence of Bags (o1 +^ o2) ;
A17: dom (decomp b2) = dom (divisors b2) by PRE_POLY:def 17;
assume A18: i in dom (divisors b1) ; :: thesis:
then consider a1', b1' being Element of Bags o1, Gi being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A19: Gi = G /. i and
A20: (decomp b1) /. i = <*a1',b1'*> and
A21: len Gi = len (decomp b2) and
A22: for m being Nat st m in dom Gi holds
ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Gi /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) by A2, A15;
take a1' ; :: thesis:
take Fk ; :: thesis:
thus Fk = F /. i ; :: thesis:
thus (divisors b1) /. i = a1' by A15, A18, A20, PRE_POLY:70; :: thesis:
A23: i in Seg (len G) by A1, A15, A18, FINSEQ_1:def 3;
then A24: dom (F /. i) = dom (G . i) by A13;
hence len Fk = len (G . i) by FINSEQ_3:31
.= len (decomp b2) by A1, A15, A18, A19, A21, PARTFUN1:def 8
.= len (divisors b2) by A17, FINSEQ_3:31 ;
:: thesis:
let m be Nat; :: thesis:
assume A25: m in dom Fk ; :: thesis:
then consider p being Element of 2 -tuples_on (Bags (o1 +^ o2)) such that
A26: p = (G . i) . m and
A27: (F /. i) . m = p . 1 by A13, A23;
A28: G . i = G /. i by A1, A15, A18, PARTFUN1:def 8;
then consider a1'', b1'' being Element of Bags o2 such that
A29: (decomp b2) /. m = <*a1'',b1''*> and
A30: Gi /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> by A19, A22, A24, A25;
A31: p = <*(a1' +^ a1''),(b1' +^ b1'')*> by A19, A24, A28, A25, A30, A26, PARTFUN1:def 8;
take a1'' ; :: thesis:
m in dom (decomp b2) by A19, A21, A24, A28, A25, FINSEQ_3:31;
hence (divisors b2) /. m = a1'' by A29, PRE_POLY:70; :: thesis:
thus Fk /. m = Fk . m by A25, PARTFUN1:def 8
.= a1' +^ a1'' by A27, A31, FINSEQ_1:61 ; :: thesis:

end;

dom (decomp b2) = dom (divisors b2) by PRE_POLY:def 17;
then A32: len (decomp b2) = len (divisors b2) by FINSEQ_3:31;
A33: for j being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j

proof

let j be Nat; :: thesis:
assume A34: j in dom (Card F) ; :: thesis:
then A35: j in dom G by A14, CARD_3:def 2;
A36: dom (Card F) = dom F by CARD_3:def 2;
then A37: (Card F) . j = card (F . j) by A34, CARD_3:def 2;
j in dom (decomp b1) by A1, A12, A34, A36, FINSEQ_1:def 3;
then A38: ( ex a1' being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. j & (divisors b1) /. j = 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'' ) ) ) & ex a2', b2' being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a2',b2'*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a2'', b2'' being Element of Bags o2 st
( (decomp b2) /. m = <*a2'',b2''*> & Gk /. m = <*(a2' +^ a2''),(b2' +^ b2'')*> ) ) ) ) by A2, A15, A16;
card (F . j) = card (F /. j) by A34, A36, PARTFUN1:def 8
.= card (G . j) by A32, A35, A38, PARTFUN1:def 8 ;
hence (Card F) . j = (Card G) . j by A35, A37, CARD_3:def 2; :: thesis:

end;

reconsider bb = b1 +^ b2 as bag of o1 +^ o2 ;
reconsider FG = FlattenSeq G as FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) ;
len (Card F) = len (Card G) by A14, FINSEQ_3:31;
then A39: Card F = Card G by A33, FINSEQ_2:10;
then A40: len FG = len (FlattenSeq F) by PRE_POLY:28;
dom (decomp b1) = dom (divisors b1) by PRE_POLY:def 17;
then dom F = dom (divisors b1) by A1, A12, FINSEQ_1:def 3;
then A41: divisors (b1 +^ b2) = FlattenSeq F by A16, Th12;
A42: dom (decomp b1) = dom (divisors b1) by PRE_POLY:def 17;
A43: for i being Element of NAT
for p being bag of o1 +^ o2 st i in dom FG & p = (divisors bb) /. i holds
FG /. i = <*p,(bb -' p)*>

proof

let k be Element of NAT ; :: thesis:
let p be bag of o1 +^ o2; :: thesis:
assume that
A44: k in dom FG and
A45: p = (divisors bb) /. k ; :: thesis:
consider i, j being Element of NAT such that
A46: i in dom G and
A47: j in dom (G . i) and
A48: k = (Sum (Card (G | (i -' 1)))) + j and
A49: (G . i) . j = FG . k by A44, PRE_POLY:29;
consider fa1 being Element of Bags o1, Fk being FinSequence of Bags (o1 +^ o2) such that
A50: Fk = F /. i and
A51: (divisors b1) /. i = fa1 and
len Fk = len (divisors b2) and
A52: for m being Nat st m in dom Fk holds
ex fa1' being Element of Bags o2 st
( (divisors b2) /. m = fa1' & Fk /. m = fa1 +^ fa1' ) by A1, A16, A42, A46;
consider a1', b1' being Element of Bags o1, Gi being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) such that
A53: Gi = G /. i and
A54: (decomp b1) /. i = <*a1',b1'*> and
A55: len Gi = len (decomp b2) and
A56: for m being Nat st m in dom Gi holds
ex a1'', b1'' being Element of Bags o2 st
( (decomp b2) /. m = <*a1'',b1''*> & Gi /. m = <*(a1' +^ a1''),(b1' +^ b1'')*> ) by A1, A2, A46;
A57: a1' = fa1 by A1, A46, A54, A51, PRE_POLY:70;
then A58: <*a1',b1'*> = <*a1',(b1 -' a1')*> by A1, A46, A54, A51, PRE_POLY:def 17;
A59: j in dom Gi by A46, A47, A53, PARTFUN1:def 8;
then consider a1'', b1'' being Element of Bags o2 such that
A60: (decomp b2) /. j = <*a1'',b1''*> and
A61: Gi /. j = <*(a1' +^ a1''),(b1' +^ b1'')*> by A56;
reconsider b2a1 = b2 -' a1'' as Element of Bags o2 by PRE_POLY:def 12;
reconsider b1a1 = b1 -' a1' as Element of Bags o1 by PRE_POLY:def 12;
k in dom (FlattenSeq F) by A40, A44, FINSEQ_3:31;
then consider i', j' being Element of NAT such that
A62: i' in dom F and
A63: j' in dom (F . i') and
A64: k = (Sum (Card (F | (i' -' 1)))) + j' and
A65: (F . i') . j' = (FlattenSeq F) . k by PRE_POLY:29;
A66: ( Card (G | (i -' 1)) = (Card G) | (i -' 1) & Card (F | (i' -' 1)) = (Card F) | (i' -' 1) ) by POLYNOM3:16;
then A67: i = i' by A39, A46, A47, A48, A62, A63, A64, POLYNOM3:22;
A68: j = j' by A39, A46, A47, A48, A62, A63, A64, A66, POLYNOM3:22;
then A69: j in dom Fk by A62, A63, A67, A50, PARTFUN1:def 8;
then consider fa1' being Element of Bags o2 such that
A70: (divisors b2) /. j = fa1' and
A71: Fk /. j = fa1 +^ fa1' by A52;
A72: j in dom (decomp b2) by A55, A59, FINSEQ_3:31;
then A73: a1'' = fa1' by A60, A70, PRE_POLY:70;
then A74: <*a1'',b1''*> = <*a1'',(b2 -' a1'')*> by A60, A70, A72, PRE_POLY:def 17;
k in dom (FlattenSeq F) by A40, A44, FINSEQ_3:31;
then A75: p = (F . i) . j by A41, A45, A65, A67, A68, PARTFUN1:def 8
.= Fk . j by A62, A67, A50, PARTFUN1:def 8
.= a1' +^ a1'' by A69, A71, A57, A73, PARTFUN1:def 8 ;
then A76: bb -' p = b1a1 +^ b2a1 by Th13
.= b1' +^ b2a1 by A58, FINSEQ_1:98
.= b1' +^ b1'' by A74, FINSEQ_1:98 ;
thus FG /. k = (G . i) . j by A44, A49, PARTFUN1:def 8
.= Gi . j by A46, A53, PARTFUN1:def 8
.= <*p,(bb -' p)*> by A59, A61, A75, A76, PARTFUN1:def 8 ; :: thesis:

end;

dom FG = dom (divisors bb) by A41, A40, FINSEQ_3:31;
hence decomp (b1 +^ b2) = FlattenSeq G by A43, PRE_POLY:def 17; :: thesis: