let L be comRing; :: thesis: for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)

let b1, b2 be bag of the carrier of L; :: thesis: poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)

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;

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

let b1, b2 be bag of the carrier of L; :: thesis: poly_with_roots (b1 + b2) = (poly_with_roots b1) *' (poly_with_roots b2)

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: for x being object holds card (Coim ((FlattenSeq f),x)) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),x))

then
FlattenSeq f,(FlattenSeq f1) ^ (FlattenSeq f2) are_fiberwise_equipotent
by CLASSES1:def 10;let x be object ; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

end;per cases
( x in rng (FlattenSeq f) or not x in rng (FlattenSeq f) )
;

end;

suppose
x in rng (FlattenSeq f)
; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

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;

end;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
( ( s /. i in support b1 & not s /. i in support b2 ) or ( not s /. i in support b1 & s /. i in support b2 ) or ( s /. i in support b1 & s /. i in support b2 ) )
by A1, A24, XBOOLE_0:def 3;

end;

suppose A26:
( s /. i in support b1 & not s /. i in support b2 )
; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

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

end;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: verum

suppose A28:
( not s /. i in support b1 & s /. i in support b2 )
; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

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

end;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: verum

suppose A30:
( s /. i in support b1 & s /. i in support b2 )
; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

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

end;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: verum

suppose A32:
not x in rng (FlattenSeq f)
; :: thesis: card (Coim ((FlattenSeq f),b_{1})) = card (Coim (((FlattenSeq f1) ^ (FlattenSeq f2)),b_{1}))

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

end;

now :: thesis: not x in rng ((FlattenSeq f1) ^ (FlattenSeq f2))

then
((FlattenSeq f1) ^ (FlattenSeq f2)) " {x} = {}
by FUNCT_1:72;assume
x in rng ((FlattenSeq f1) ^ (FlattenSeq f2))
; :: thesis: contradiction

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

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

per cases
( x in rng (FlattenSeq f1) or x in rng (FlattenSeq f2) )
by A33, XBOOLE_0:def 3;

end;

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

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

end;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: verum

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

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

end;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: verum

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

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