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

now

let x be set ; :: 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:11;
consider i, j being Element of 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, POLYNOM1:32;
f . i = fpoly_mult_root (s /. i),((b1 + b2) . (s /. i)) by A3, A20;
then A23: (f . i) . j = <%(- (s /. i)),(1. L)%> by A21, Def10;
i in dom s by A1, A17, A20, FINSEQ_3:31;
then ( s . i = s /. i & s . i in rng s ) by FUNCT_1:12, PARTFUN1:def 8;
then A24: s /. i in support (b1 + b2) by A2, FUNCT_2:def 3;
A25: card (((FlattenSeq f1) ^ (FlattenSeq f2)) " {x}) = (card ((FlattenSeq f1) " {x})) + (card ((FlattenSeq f2) " {x})) by FINSEQ_3:63;

per cases by A13, 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 A9, A10, A11, A19, A22, A23, Th65;
thus card (Coim (FlattenSeq f),x) = (b1 + b2) . (s /. i) by A1, A2, A3, A19, A22, A23, A24, Th65
.= (b1 . (s /. i)) + (b2 . (s /. i)) by POLYNOM1:def 5
.= (b1 . (s /. i)) + 0 by A26, POLYNOM1:def 7
.= card (Coim ((FlattenSeq f1) ^ (FlattenSeq f2)),x) by A5, A6, A7, A19, A22, A23, A25, A26, A27, Th65 ; :: 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 A9, A10, A11, A19, A22, A23, Th65;
thus card (Coim (FlattenSeq f),x) = (b1 + b2) . (s /. i) by A1, A2, A3, A19, A22, A23, A24, Th65
.= (b1 . (s /. i)) + (b2 . (s /. i)) by POLYNOM1:def 5
.= 0 + (b2 . (s /. i)) by A28, POLYNOM1:def 7
.= card (Coim ((FlattenSeq f1) ^ (FlattenSeq f2)),x) by A5, A6, A7, A19, A22, A23, A25, A28, A29, Th65 ; :: 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 A9, A10, A11, A19, A22, A23, Th65;
thus card (Coim (FlattenSeq f),x) = (b1 + b2) . (s /. i) by A1, A2, A3, A19, A22, A23, A24, Th65
.= (b1 . (s /. i)) + (b2 . (s /. i)) by POLYNOM1:def 5
.= card (Coim ((FlattenSeq f1) ^ (FlattenSeq f2)),x) by A5, A6, A7, A19, A22, A23, A25, A30, A31, Th65 ; :: thesis:

end;

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

now

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

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:11;
consider i, j being Element of 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, POLYNOM1:32;
f1 . i = fpoly_mult_root (s1 /. i),(b1 . (s1 /. i)) by A7, A36;
then A39: (f1 . i) . j = <%(- (s1 /. i)),(1. L)%> by A37, Def10;
len s1 = card (support b1) by A6, Def1;
then i in dom s1 by A5, A36, FINSEQ_3:31;
then ( s1 . i = s1 /. i & s1 . i in rng s1 ) by FUNCT_1:12, PARTFUN1:def 8;
then s1 /. i in support b1 by A6, FUNCT_2:def 3;
then A40: s1 /. i in support (b1 + b2) by A13, XBOOLE_0:def 3;
then s1 /. i in rng s by A2, FUNCT_2:def 3;
then consider l being Nat such that
A41: l in dom s and
A42: s . l = s1 /. i by FINSEQ_2:11;
A43: l in dom f by A1, A17, A41, FINSEQ_3:31;
then A44: f . l = fpoly_mult_root (s /. l),((b1 + b2) . (s /. l)) by A3;
A45: s . l = s /. l by A41, PARTFUN1:def 8;
(b1 + b2) . (s1 /. i) <> 0 by A40, POLYNOM1:def 7;
then A46: 0 + 1 <= (b1 + b2) . (s1 /. i) by NAT_1:13;
len (f . l) = (b1 + b2) . (s /. l) by A44, Def10;
then A47: 1 in dom (f . l) by A42, A45, A46, FINSEQ_3:27;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A43, POLYNOM1:33;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:12;
hence contradiction by A32, A35, A38, A39, A42, A44, A45, A47, Def10; :: 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:11;
consider i, j being Element of 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, POLYNOM1:32;
f2 . i = fpoly_mult_root (s2 /. i),(b2 . (s2 /. i)) by A11, A50;
then A53: (f2 . i) . j = <%(- (s2 /. i)),(1. L)%> by A51, Def10;
len s2 = card (support b2) by A10, Def1;
then i in dom s2 by A9, A50, FINSEQ_3:31;
then ( s2 . i = s2 /. i & s2 . i in rng s2 ) by FUNCT_1:12, PARTFUN1:def 8;
then s2 /. i in support b2 by A10, FUNCT_2:def 3;
then A54: s2 /. i in support (b1 + b2) by A13, XBOOLE_0:def 3;
then s2 /. i in rng s by A2, FUNCT_2:def 3;
then consider l being Nat such that
A55: l in dom s and
A56: s . l = s2 /. i by FINSEQ_2:11;
A57: l in dom f by A1, A17, A55, FINSEQ_3:31;
then A58: f . l = fpoly_mult_root (s /. l),((b1 + b2) . (s /. l)) by A3;
A59: s . l = s /. l by A55, PARTFUN1:def 8;
(b1 + b2) . (s2 /. i) <> 0 by A54, POLYNOM1:def 7;
then A60: 0 + 1 <= (b1 + b2) . (s2 /. i) by NAT_1:13;
len (f . l) = (b1 + b2) . (s /. l) by A58, Def10;
then A61: 1 in dom (f . l) by A56, A59, A60, FINSEQ_3:27;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom (FlattenSeq f) & (f . l) . 1 = (FlattenSeq f) . ((Sum (Card (f | (l -' 1)))) + 1) ) by A57, POLYNOM1:33;
then (f . l) . 1 in rng (FlattenSeq f) by FUNCT_1:12;
hence contradiction by A32, A49, A52, A53, A56, A58, A59, A61, Def10; :: thesis:

end;

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

end;

then FlattenSeq f,(FlattenSeq f1) ^ (FlattenSeq f2) are_fiberwise_equipotent by CLASSES1:def 9;
then consider p being Permutation of (dom (FlattenSeq f)) such that
A62: FlattenSeq f = ((FlattenSeq f1) ^ (FlattenSeq f2)) * p by A16, RFINSEQ:17;
thus poly_with_roots (b1 + b2) = Product ((FlattenSeq f1) ^ (FlattenSeq f2)) by A4, A16, A62, Th18
.= (Product (FlattenSeq f1)) * (Product (FlattenSeq f2)) by GROUP_4:8
.= (poly_with_roots b1) *' (poly_with_roots b2) by A8, A12, POLYNOM3:def 12 ; :: thesis: