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 S_{1}[ 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 S_{1}[k,p]

A12: dom F = Seg (len G) and

A13: for i being Nat st i in Seg (len G) holds

S_{1}[i,F /. i]
from RECDEF_1:sch 17(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 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 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

reconsider FG = FlattenSeq G as FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) ;

len (Card F) = len (Card G) by A14, FINSEQ_3:29;

then A39: Card F = Card G by A33, FINSEQ_2:9;

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

hence decomp (b1 +^ b2) = FlattenSeq G by A43, PRE_POLY:def 17; :: thesis: verum

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 S

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 S

proof

consider F being FinSequence of (Bags (o1 +^ o2)) * such that
let k be Nat; :: thesis: ( k in Seg (len G) implies ex p being Element of (Bags (o1 +^ o2)) * st S_{1}[k,p] )

assume A4: k in Seg (len G) ; :: thesis: ex p being Element of (Bags (o1 +^ o2)) * st S_{1}[k,p]

defpred S_{2}[ 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 S_{2}[j,x]

A7: dom p = Seg (len (G . k)) and

A8: for j being Nat st j in Seg (len (G . k)) holds

S_{2}[j,p /. j]
from RECDEF_1:sch 17(A5);

reconsider p = p as Element of (Bags (o1 +^ o2)) * by FINSEQ_1:def 11;

take p ; :: thesis: S_{1}[k,p]

thus dom p = dom (G . k) by A7, FINSEQ_1:def 3; :: 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 A9, A11, PARTFUN1:def 6; :: thesis: verum

end;assume A4: k in Seg (len G) ; :: thesis: ex p being Element of (Bags (o1 +^ o2)) * st S

defpred S

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

proof

consider p being FinSequence of Bags (o1 +^ o2) such that
k in dom G
by A4, FINSEQ_1:def 3;

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 S_{2}[j,x] )

assume j in Seg (len (G . k)) ; :: thesis: ex x being Element of Bags (o1 +^ o2) st S_{2}[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: S_{2}[j,x]

thus S_{2}[j,x]
; :: thesis: verum

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

assume j in Seg (len (G . k)) ; :: thesis: ex x being Element of Bags (o1 +^ o2) st S

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

thus S

A7: dom p = Seg (len (G . k)) and

A8: for j being Nat st j in Seg (len (G . k)) holds

S

reconsider p = p as Element of (Bags (o1 +^ o2)) * by FINSEQ_1:def 11;

take p ; :: thesis: S

thus dom p = dom (G . k) by A7, FINSEQ_1:def 3; :: 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 A9, A11, PARTFUN1:def 6; :: thesis: verum

A12: dom F = Seg (len G) and

A13: for i being Nat st i in Seg (len G) holds

S

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

dom (decomp b2) = dom (divisors b2)
by PRE_POLY:def 17;
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 A2, A15;

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 A15, A18, A20, PRE_POLY:70; :: 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 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:29

.= len (decomp b2) by A1, A15, A18, A19, A21, PARTFUN1:def 6

.= len (divisors b2) by A17, FINSEQ_3:29 ;

:: 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 A13, A23;

A28: G . i = G /. i by A1, A15, A18, PARTFUN1:def 6;

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 A19, A24, A28, A25, A30, A26, PARTFUN1:def 6;

take a199 ; :: thesis: ( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )

m in dom (decomp b2) by A19, A21, A24, A28, A25, FINSEQ_3:29;

hence (divisors b2) /. m = a199 by A29, PRE_POLY:70; :: thesis: Fk /. m = a19 +^ a199

thus Fk /. m = Fk . m by A25, PARTFUN1:def 6

.= a19 +^ a199 by A27, A31, FINSEQ_1:44 ; :: thesis: verum

end;( 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 A2, A15;

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 A15, A18, A20, PRE_POLY:70; :: 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 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:29

.= len (decomp b2) by A1, A15, A18, A19, A21, PARTFUN1:def 6

.= len (divisors b2) by A17, FINSEQ_3:29 ;

:: 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 A13, A23;

A28: G . i = G /. i by A1, A15, A18, PARTFUN1:def 6;

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 A19, A24, A28, A25, A30, A26, PARTFUN1:def 6;

take a199 ; :: thesis: ( (divisors b2) /. m = a199 & Fk /. m = a19 +^ a199 )

m in dom (decomp b2) by A19, A21, A24, A28, A25, FINSEQ_3:29;

hence (divisors b2) /. m = a199 by A29, PRE_POLY:70; :: thesis: Fk /. m = a19 +^ a199

thus Fk /. m = Fk . m by A25, PARTFUN1:def 6

.= a19 +^ a199 by A27, A31, FINSEQ_1:44 ; :: thesis: verum

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

reconsider bb = b1 +^ b2 as bag of o1 +^ o2 ;
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 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 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 A34, A36, PARTFUN1:def 6

.= card (G . j) by A32, A35, A38, PARTFUN1:def 6 ;

hence (Card F) . j = (Card G) . j by A35, A37, CARD_3:def 2; :: thesis: verum

end;assume A34: j in dom (Card F) ; :: thesis: (Card F) . j = (Card G) . j

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 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 A34, A36, PARTFUN1:def 6

.= card (G . j) by A32, A35, A38, PARTFUN1:def 6 ;

hence (Card F) . j = (Card G) . j by A35, A37, CARD_3:def 2; :: thesis: verum

reconsider FG = FlattenSeq G as FinSequence of 2 -tuples_on (Bags (o1 +^ o2)) ;

len (Card F) = len (Card G) by A14, FINSEQ_3:29;

then A39: Card F = Card G by A33, FINSEQ_2:9;

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

dom FG = dom (divisors bb)
by A41, A40, FINSEQ_3:29;
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 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 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 A1, A46, A54, A51, PRE_POLY:70;

then A58: <*a19,b19*> = <*a19,(b1 -' a19)*> by A1, A46, A54, A51, PRE_POLY:def 17;

A59: j in dom Gi by A46, A47, A53, PARTFUN1:def 6;

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 (FlattenSeq F) by A40, A44, FINSEQ_3:29;

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 = (FlattenSeq F) . 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 A39, A46, A47, A48, A62, A63, A64, POLYNOM3:22;

A68: j = j9 by A39, A46, A47, A48, A62, A63, A64, A66, POLYNOM3:22;

then A69: j in dom Fk by A62, A63, A67, A50, PARTFUN1:def 6;

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 A55, A59, FINSEQ_3:29;

then A73: a199 = fa19 by A60, A70, PRE_POLY:70;

then A74: <*a199,b199*> = <*a199,(b2 -' a199)*> by A60, A70, A72, PRE_POLY:def 17;

k in dom (FlattenSeq F) by A40, A44, FINSEQ_3:29;

then A75: p = (F . i) . j by A41, A45, A65, A67, A68, PARTFUN1:def 6

.= Fk . j by A62, A67, A50, PARTFUN1:def 6

.= a19 +^ a199 by A69, A71, A57, A73, PARTFUN1:def 6 ;

then A76: bb -' p = b1a1 +^ b2a1 by Th13

.= b19 +^ b2a1 by A58, FINSEQ_1:77

.= b19 +^ b199 by A74, FINSEQ_1:77 ;

thus FG /. k = (G . i) . j by A44, A49, PARTFUN1:def 6

.= Gi . j by A46, A53, PARTFUN1:def 6

.= <*p,(bb -' p)*> by A59, A61, A75, A76, PARTFUN1:def 6 ; :: thesis: verum

end;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 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 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 A1, A46, A54, A51, PRE_POLY:70;

then A58: <*a19,b19*> = <*a19,(b1 -' a19)*> by A1, A46, A54, A51, PRE_POLY:def 17;

A59: j in dom Gi by A46, A47, A53, PARTFUN1:def 6;

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 (FlattenSeq F) by A40, A44, FINSEQ_3:29;

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 = (FlattenSeq F) . 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 A39, A46, A47, A48, A62, A63, A64, POLYNOM3:22;

A68: j = j9 by A39, A46, A47, A48, A62, A63, A64, A66, POLYNOM3:22;

then A69: j in dom Fk by A62, A63, A67, A50, PARTFUN1:def 6;

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 A55, A59, FINSEQ_3:29;

then A73: a199 = fa19 by A60, A70, PRE_POLY:70;

then A74: <*a199,b199*> = <*a199,(b2 -' a199)*> by A60, A70, A72, PRE_POLY:def 17;

k in dom (FlattenSeq F) by A40, A44, FINSEQ_3:29;

then A75: p = (F . i) . j by A41, A45, A65, A67, A68, PARTFUN1:def 6

.= Fk . j by A62, A67, A50, PARTFUN1:def 6

.= a19 +^ a199 by A69, A71, A57, A73, PARTFUN1:def 6 ;

then A76: bb -' p = b1a1 +^ b2a1 by Th13

.= b19 +^ b2a1 by A58, FINSEQ_1:77

.= b19 +^ b199 by A74, FINSEQ_1:77 ;

thus FG /. k = (G . i) . j by A44, A49, PARTFUN1:def 6

.= Gi . j by A46, A53, PARTFUN1:def 6

.= <*p,(bb -' p)*> by A59, A61, A75, A76, PARTFUN1:def 6 ; :: thesis: verum

hence decomp (b1 +^ b2) = FlattenSeq G by A43, PRE_POLY:def 17; :: thesis: verum