let L be comRing; :: thesis:
let b1, b2 be bag of the carrier of L; :: thesis:
set b = b1 + b2;
A1: support (b1 + b2) = (support b1) \/ (support b2) by PRE_POLY:38;
consider f2 being FinSequence of the carrier of (Polynom-Ring L) * , s2 being FinSequence of L such that
A2: len f2 = card (support b2) and
A3: s2 = canFS (support b2) and
A4: for i being Element of NAT st i in dom f2 holds
f2 . i = fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i))) and
A5: poly_with_roots b2 = Product (FlattenSeq f2) by Def10;
consider f1 being FinSequence of the carrier of (Polynom-Ring L) * , s1 being FinSequence of L such that
A6: len f1 = card (support b1) and
A7: s1 = canFS (support b1) and
A8: for i being Element of NAT st i in dom f1 holds
f1 . i = fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i))) and
A9: poly_with_roots b1 = Product (FlattenSeq f1) by Def10;
consider f being FinSequence of the carrier of (Polynom-Ring L) * , s being FinSequence of L such that
A10: len f = card (support (b1 + b2)) and
A11: s = canFS (support (b1 + b2)) and
A12: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) and
A13: poly_with_roots (b1 + b2) = Product (FlattenSeq f) by Def10;
set ff = FlattenSeq f;
set ff1 = FlattenSeq f1;
set ff2 = FlattenSeq f2;
A14: len (FlattenSeq f) = degree (b1 + b2) by A10, A11, A12, Th59;
A15: len (FlattenSeq f2) = degree b2 by A2, A3, A4, Th59;
set g = (FlattenSeq f1) ^ (FlattenSeq f2);
len ((FlattenSeq f1) ^ (FlattenSeq f2)) = (len (FlattenSeq f1)) + (len (FlattenSeq f2)) by FINSEQ_1:22
.= (degree b1) + (degree b2) by A6, A7, A8, A15, Th59
.= degree (b1 + b2) by Th12 ;
then A16: dom (FlattenSeq f) = dom ((FlattenSeq f1) ^ (FlattenSeq f2)) by A14, FINSEQ_3:29;
A17: len s = card (support (b1 + b2)) by A11, FINSEQ_1:93;

now :: thesis:

let x be object ; :: thesis:

per cases ;

suppose x in rng (FlattenSeq f) ; :: thesis:

then consider k being Nat such that
A18: k in dom (FlattenSeq f) and
A19: (FlattenSeq f) . k = x by FINSEQ_2:10;
consider i, j being Nat such that
A20: i in dom f and
A21: j in dom (f . i) and
k = (Sum (Card (f | (i -' 1)))) + j and
A22: (f . i) . j = (FlattenSeq f) . k by A18, PRE_POLY:29;
f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) by A12, A20;
then A23: (f . i) . j = <%(- (s /. i)),(1. L)%> by A21, Def9;
i in dom s by A10, A17, A20, FINSEQ_3:29;
then ( s . i = s /. i & s . i in rng s ) by FUNCT_1:3, PARTFUN1:def 6;
then A24: s /. i in support (b1 + b2) by A11, FUNCT_2:def 3;
A25: card (((FlattenSeq f1) ^ (FlattenSeq f2)) " {x}) = (card ((FlattenSeq f1) " {x})) + (card ((FlattenSeq f2) " {x})) by FINSEQ_3:57;

per cases by A1, A24, XBOOLE_0:def 3;

suppose A26: ( s /. i in support b1 & not s /. i in support b2 ) ; :: thesis:

then A27: card ((FlattenSeq f2) " {x}) = 0 by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th60
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def 5
.= (b1 . (s /. i)) + 0 by A26, PRE_POLY:def 7
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A26, A27, Th60 ; :: thesis:

end;

suppose A28: ( not s /. i in support b1 & s /. i in support b2 ) ; :: thesis:

then A29: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th60
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def 5
.= 0 + (b2 . (s /. i)) by A28, PRE_POLY:def 7
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A28, A29, Th60 ; :: thesis:

end;

suppose A30: ( s /. i in support b1 & s /. i in support b2 ) ; :: thesis:

then A31: card ((FlattenSeq f2) " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((FlattenSeq f),x)) = (b1 + b2) . (s /. i) by A10, A11, A12, A19, A22, A23, A24, Th60
.= (b1 . (s /. i)) + (b2 . (s /. i)) by PRE_POLY:def 5
.= card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A6, A7, A8, A19, A22, A23, A25, A30, A31, Th60 ; :: thesis:

end;

suppose A32: not x in rng (FlattenSeq f) ; :: thesis:

now :: thesis:

assume x in rng ((FlattenSeq f1) ^ (FlattenSeq f2)) ; :: thesis:
then A33: x in (rng (FlattenSeq f1)) \/ (rng (FlattenSeq f2)) by FINSEQ_1:31;

per cases by A33, XBOOLE_0:def 3;

suppose x in rng (FlattenSeq f1) ; :: thesis:

then consider k being Nat such that
A34: k in dom (FlattenSeq f1) and
A35: (FlattenSeq f1) . k = x by FINSEQ_2:10;
consider i, j being Nat such that
A36: i in dom f1 and
A37: j in dom (f1 . i) and
k = (Sum (Card (f1 | (i -' 1)))) + j and
A38: (f1 . i) . j = (FlattenSeq f1) . k by A34, PRE_POLY:29;
f1 . i = fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i))) by A8, A36;
then A39: (f1 . i) . j = <%(- (s1 /. i)),(1. L)%> by A37, Def9;
len s1 = card (support b1) by A7, FINSEQ_1:93;
then i in dom s1 by A6, A36, FINSEQ_3:29;
then ( s1 . i = s1 /. i & s1 . i in rng s1 ) by FUNCT_1:3, PARTFUN1:def 6;
then s1 /. i in support b1 by A7, FUNCT_2:def 3;
then A40: s1 /. i in support (b1 + b2) by A1, XBOOLE_0:def 3;
then (b1 + b2) . (s1 /. i) <> 0 by PRE_POLY:def 7;
then A41: 0 + 1 <= (b1 + b2) . (s1 /. i) by NAT_1:13;
s1 /. i in rng s by A11, A40, FUNCT_2:def 3;
then consider l being Nat such that
A42: l in dom s and
A43: s . l = s1 /. i by FINSEQ_2:10;
A44: s . l = s /. l by A42, PARTFUN1:def 6;
A45: l in dom f by A10, A17, A42, FINSEQ_3:29;
then A46: f . l = fpoly_mult_root ((s /. l),((b1 + b2) . (s /. l))) by A12;
then len (f . l) = (b1 + b2) . (s /. l) by Def9;
then A47: 1 in dom (f . l) by A43, A44, A41, FINSEQ_3:25;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A45, PRE_POLY:30;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3;
hence contradiction by A32, A35, A38, A39, A43, A46, A44, A47, Def9; :: thesis:

end;

suppose x in rng (FlattenSeq f2) ; :: thesis:

then consider k being Nat such that
A48: k in dom (FlattenSeq f2) and
A49: (FlattenSeq f2) . k = x by FINSEQ_2:10;
consider i, j being Nat such that
A50: i in dom f2 and
A51: j in dom (f2 . i) and
k = (Sum (Card (f2 | (i -' 1)))) + j and
A52: (f2 . i) . j = (FlattenSeq f2) . k by A48, PRE_POLY:29;
f2 . i = fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i))) by A4, A50;
then A53: (f2 . i) . j = <%(- (s2 /. i)),(1. L)%> by A51, Def9;
len s2 = card (support b2) by A3, FINSEQ_1:93;
then i in dom s2 by A2, A50, FINSEQ_3:29;
then ( s2 . i = s2 /. i & s2 . i in rng s2 ) by FUNCT_1:3, PARTFUN1:def 6;
then s2 /. i in support b2 by A3, FUNCT_2:def 3;
then A54: s2 /. i in support (b1 + b2) by A1, XBOOLE_0:def 3;
then (b1 + b2) . (s2 /. i) <> 0 by PRE_POLY:def 7;
then A55: 0 + 1 <= (b1 + b2) . (s2 /. i) by NAT_1:13;
s2 /. i in rng s by A11, A54, FUNCT_2:def 3;
then consider l being Nat such that
A56: l in dom s and
A57: s . l = s2 /. i by FINSEQ_2:10;
A58: s . l = s /. l by A56, PARTFUN1:def 6;
A59: l in dom f by A10, A17, A56, FINSEQ_3:29;
then A60: f . l = fpoly_mult_root ((s /. l),((b1 + b2) . (s /. l))) by A12;
then len (f . l) = (b1 + b2) . (s /. l) by Def9;
then A61: 1 in dom (f . l) by A57, A58, A55, FINSEQ_3:25;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A59, PRE_POLY:30;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:3;
hence contradiction by A32, A49, A52, A53, A57, A60, A58, A61, Def9; :: thesis:

end;

then ((FlattenSeq f1) ^ (FlattenSeq f2)) " {x} = {} by FUNCT_1:72;
hence card (Coim ((FlattenSeq f),x)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x)) by A32, FUNCT_1:72; :: thesis:

end;

then FlattenSeq f,(FlattenSeq f1) ^ (FlattenSeq f2) are_fiberwise_equipotent by CLASSES1:def 10;
then ex p being Permutation of (dom (FlattenSeq f)) st FlattenSeq f = ((FlattenSeq f1) ^ (FlattenSeq f2)) * p by A16, RFINSEQ:4;
hence poly_with_roots (b1 + b2) = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by A13, A16, Th13
.= (Product (FlattenSeq f1)) * (Product (FlattenSeq f2)) by GROUP_4:5
.= (poly_with_roots b1) *' (poly_with_roots b2) by A9, A5, POLYNOM3:def 10 ;
:: thesis: