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 (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G

let b1 be Element of Bags o1; :: thesis: for b2 being Element of Bags o2
for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G

let b2 be Element of Bags o2; :: thesis: for G being FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * st dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) holds
decomp (b1 +^ b2) = FlattenSeq G

let G be FinSequence of (2 -tuples_on (Bags (o1 +^ o2))) * ; :: thesis: ( dom G = dom (decomp b1) & ( for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ) implies decomp (b1 +^ b2) = FlattenSeq G )

assume that
A1: dom G = dom (decomp b1) and
A2: for i being Nat st i in dom (decomp b1) holds
ex a19, b19 being Element of Bags o1 ex Fk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Fk = G /. i & (decomp b1) /. i = <*a19,b19*> & len Fk = len (decomp b2) & ( for m being Nat st m in dom Fk holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Fk /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) ) ) ; :: thesis: decomp (b1 +^ b2) = FlattenSeq G
defpred S1[ 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 Nat st k in Seg (len G) holds
ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p]
proof
let k be Nat; :: thesis: ( k in Seg (len G) implies ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p] )
assume A4: k in Seg (len G) ; :: thesis: ex p being Element of (Bags (o1 +^ o2)) * st S1[k,p]
defpred S2[ 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 Nat st j in Seg (len (G . k)) holds
ex x being Element of Bags (o1 +^ o2) st S2[j,x]
proof
k in dom G by ;
then A6: G . k in rng G by FUNCT_1:3;
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 Nat; :: thesis: ( j in Seg (len (G . k)) implies ex x being Element of Bags (o1 +^ o2) st S2[j,x] )
assume j in Seg (len (G . k)) ; :: thesis: ex x being Element of Bags (o1 +^ o2) st S2[j,x]
then j in dom (G . k) by FINSEQ_1:def 3;
then (G . k) . j = Gk /. j by PARTFUN1:def 6;
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:100;
then reconsider x = q . 1 as Element of Bags (o1 +^ o2) by FINSEQ_1:44;
take x ; :: thesis: S2[j,x]
thus S2[j,x] ; :: thesis: verum
end;
consider p being FinSequence of Bags (o1 +^ o2) such that
A7: dom p = Seg (len (G . k)) and
A8: for j being Nat st j in Seg (len (G . k)) holds
S2[j,p /. j] from reconsider p = p as Element of (Bags (o1 +^ o2)) * by FINSEQ_1:def 11;
take p ; :: thesis: S1[k,p]
thus dom p = dom (G . k) by ; :: thesis: for j being Nat st j in dom p holds
ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 )

let j be Nat; :: thesis: ( j in dom p implies ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 ) )

assume A9: j in dom p ; :: thesis: ex p being Element of 2 -tuples_on (Bags (o1 +^ o2)) st
( p = (G . k) . j & p . j = p . 1 )

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: ( q = (G . k) . j & p . j = q . 1 )
thus q = (G . k) . j by A10; :: thesis: p . j = q . 1
thus p . j = q . 1 by ; :: thesis: verum
end;
consider F being FinSequence of (Bags (o1 +^ o2)) * such that
A12: dom F = Seg (len G) and
A13: for i being Nat st i in Seg (len G) holds
S1[i,F /. i] from A14: dom (Card F) = dom F by CARD_3:def 2
.= dom G by
.= 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 a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. 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 ) ) )
proof
let i be Nat; :: thesis: ( i in dom (divisors b1) implies ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. 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 ) ) ) )

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: ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. 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 ) ) )

then consider a19, b19 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 = <*a19,b19*> and
A21: len Gi = len (decomp b2) and
A22: for m being Nat st m in dom Gi holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Gi /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) by ;
take a19 ; :: thesis: ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. 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 ) ) )

take Fk ; :: thesis: ( Fk = F /. 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 ) ) )

thus Fk = F /. i ; :: thesis: ( (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 ) ) )

thus (divisors b1) /. i = a19 by ; :: thesis: ( 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 ) ) )

A23: i in Seg (len G) by ;
then A24: dom (F /. i) = dom (G . i) by A13;
hence len Fk = len (G . i) by FINSEQ_3:29
.= len (decomp b2) by
.= len (divisors b2) by ;
:: thesis: 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 )

let m be Nat; :: thesis: ( m in dom Fk implies ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 ) )

assume A25: m in dom Fk ; :: thesis: ex a199 being Element of Bags o2 st
( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )

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 ;
A28: G . i = G /. i by ;
then consider a199, b199 being Element of Bags o2 such that
A29: (decomp b2) /. m = <*a199,b199*> and
A30: Gi /. m = <*(a19 +^ a199),(b19 +^ b199)*> by A19, A22, A24, A25;
A31: p = <*(a19 +^ a199),(b19 +^ b199)*> by ;
take a199 ; :: thesis: ( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )
m in dom (decomp b2) by ;
hence (divisors b2) /. m = a199 by ; :: thesis: Fk /. m = a19 +^ a199
thus Fk /. m = Fk . m by
.= a19 +^ a199 by ; :: thesis: verum
end;
dom (decomp b2) = dom (divisors b2) by PRE_POLY:def 17;
then A32: len (decomp b2) = len (divisors b2) by FINSEQ_3:29;
A33: for j being Nat st j in dom (Card F) holds
(Card F) . j = (Card G) . j
proof
let j be Nat; :: thesis: ( j in dom (Card F) implies (Card F) . j = (Card G) . j )
assume A34: j in dom (Card F) ; :: thesis: (Card F) . j = (Card G) . j
then A35: j in dom G by ;
A36: dom (Card F) = dom F by CARD_3:def 2;
then A37: (Card F) . j = card (F . j) by ;
j in dom (decomp b1) by ;
then A38: ( ex a19 being Element of Bags o1 ex Fk being FinSequence of Bags (o1 +^ o2) st
( Fk = F /. j & (divisors b1) /. j = 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 ) ) ) & ex a29, b29 being Element of Bags o1 ex Gk being FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) st
( Gk = G /. j & (decomp b1) /. j = <*a29,b29*> & len Gk = len (decomp b2) & ( for m being Nat st m in dom Gk holds
ex a299, b299 being Element of Bags o2 st
( (decomp b2) /. m = <*a299,b299*> & Gk /. m = <*(a29 +^ a299),(b29 +^ b299)*> ) ) ) ) by A2, A15, A16;
card (F . j) = card (F /. j) by
.= card (G . j) by ;
hence (Card F) . j = (Card G) . j by ; :: thesis: verum
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 ;
then A39: Card F = Card G by ;
then A40: len FG = len () by PRE_POLY:28;
dom (decomp b1) = dom (divisors b1) by PRE_POLY:def 17;
then dom F = dom (divisors b1) by ;
then A41: divisors (b1 +^ b2) = FlattenSeq F by ;
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: for p being bag of o1 +^ o2 st k in dom FG & p = (divisors bb) /. k holds
FG /. k = <*p,(bb -' p)*>

let p be bag of o1 +^ o2; :: thesis: ( k in dom FG & p = (divisors bb) /. k implies FG /. k = <*p,(bb -' p)*> )
assume that
A44: k in dom FG and
A45: p = (divisors bb) /. k ; :: thesis: FG /. k = <*p,(bb -' p)*>
consider i, j being 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 ;
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 fa19 being Element of Bags o2 st
( (divisors b2) /. m = fa19 & Fk /. m = fa1 +^ fa19 ) by A1, A16, A42, A46;
consider a19, b19 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 = <*a19,b19*> and
A55: len Gi = len (decomp b2) and
A56: for m being Nat st m in dom Gi holds
ex a199, b199 being Element of Bags o2 st
( (decomp b2) /. m = <*a199,b199*> & Gi /. m = <*(a19 +^ a199),(b19 +^ b199)*> ) by A1, A2, A46;
A57: a19 = fa1 by ;
then A58: <*a19,b19*> = <*a19,(b1 -' a19)*> by ;
A59: j in dom Gi by ;
then consider a199, b199 being Element of Bags o2 such that
A60: (decomp b2) /. j = <*a199,b199*> and
A61: Gi /. j = <*(a19 +^ a199),(b19 +^ b199)*> by A56;
reconsider b2a1 = b2 -' a199 as Element of Bags o2 by PRE_POLY:def 12;
reconsider b1a1 = b1 -' a19 as Element of Bags o1 by PRE_POLY:def 12;
k in dom () by ;
then consider i9, j9 being Nat such that
A62: i9 in dom F and
A63: j9 in dom (F . i9) and
A64: k = (Sum (Card (F | (i9 -' 1)))) + j9 and
A65: (F . i9) . j9 = () . k by PRE_POLY:29;
A66: ( Card (G | (i -' 1)) = (Card G) | (i -' 1) & Card (F | (i9 -' 1)) = (Card F) | (i9 -' 1) ) by POLYNOM3:16;
then A67: i = i9 by ;
A68: j = j9 by ;
then A69: j in dom Fk by ;
then consider fa19 being Element of Bags o2 such that
A70: (divisors b2) /. j = fa19 and
A71: Fk /. j = fa1 +^ fa19 by A52;
A72: j in dom (decomp b2) by ;
then A73: a199 = fa19 by ;
then A74: <*a199,b199*> = <*a199,(b2 -' a199)*> by ;
k in dom () by ;
then A75: p = (F . i) . j by
.= Fk . j by
.= a19 +^ a199 by ;
then A76: bb -' p = b1a1 +^ b2a1 by Th13
.= b19 +^ b2a1 by
.= b19 +^ b199 by ;
thus FG /. k = (G . i) . j by
.= Gi . j by
.= <*p,(bb -' p)*> by ; :: thesis: verum
end;
dom FG = dom (divisors bb) by ;
hence decomp (b1 +^ b2) = FlattenSeq G by ; :: thesis: verum