let L be comRing; :: thesis: for b1, b2 being bag of the carrier of L holds poly_with_roots (b1 + b2) = () *' ()
let b1, b2 be bag of the carrier of L; :: thesis: poly_with_roots (b1 + 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 () * , 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 () by Def10;
consider f1 being FinSequence of the carrier of () * , 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 () by Def10;
consider f being FinSequence of the carrier of () * , 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 () by Def10;
set ff = FlattenSeq f;
set ff1 = FlattenSeq f1;
set ff2 = FlattenSeq f2;
A14: len () = degree (b1 + b2) by ;
A15: len () = degree b2 by A2, A3, A4, Th59;
set g = () ^ ();
len (() ^ ()) = (len ()) + (len ()) by FINSEQ_1:22
.= (degree b1) + (degree b2) by A6, A7, A8, A15, Th59
.= degree (b1 + b2) by Th12 ;
then A16: dom () = dom (() ^ ()) by ;
A17: len s = card (support (b1 + b2)) by ;
now :: thesis: for x being object holds card (Coim ((),x)) = card (Coim ((() ^ ()),x))
let x be object ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
per cases ( x in rng () or not x in rng () ) ;
suppose x in rng () ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
then consider k being Nat such that
A18: k in dom () 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 = () . k by ;
f . i = fpoly_mult_root ((s /. i),((b1 + b2) . (s /. i))) by ;
then A23: (f . i) . j = <%(- (s /. i)),(1. L)%> by ;
i in dom s by ;
then ( s . i = s /. i & s . i in rng s ) by ;
then A24: s /. i in support (b1 + b2) by ;
A25: card ((() ^ ()) " {x}) = (card (() " {x})) + (card (() " {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 ;
suppose A26: ( s /. i in support b1 & not s /. i in support b2 ) ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
then A27: card (() " {x}) = 0 by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((),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
.= card (Coim ((() ^ ()),x)) by A6, A7, A8, A19, A22, A23, A25, A26, A27, Th60 ; :: thesis: verum
end;
suppose A28: ( not s /. i in support b1 & s /. i in support b2 ) ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
then A29: card (() " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((),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
.= card (Coim ((() ^ ()),x)) by A6, A7, A8, A19, A22, A23, A25, A28, A29, Th60 ; :: thesis: verum
end;
suppose A30: ( s /. i in support b1 & s /. i in support b2 ) ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
then A31: card (() " {x}) = b2 . (s /. i) by A2, A3, A4, A19, A22, A23, Th60;
thus card (Coim ((),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 ((() ^ ()),x)) by A6, A7, A8, A19, A22, A23, A25, A30, A31, Th60 ; :: thesis: verum
end;
end;
end;
suppose A32: not x in rng () ; :: thesis: card (Coim ((),b1)) = card (Coim ((() ^ ()),b1))
now :: thesis: not x in rng (() ^ ())
assume x in rng (() ^ ()) ; :: thesis: contradiction
then A33: x in (rng ()) \/ (rng ()) by FINSEQ_1:31;
per cases ( x in rng () or x in rng () ) by ;
suppose x in rng () ; :: thesis: contradiction
then consider k being Nat such that
A34: k in dom () 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 = () . k by ;
f1 . i = fpoly_mult_root ((s1 /. i),(b1 . (s1 /. i))) by ;
then A39: (f1 . i) . j = <%(- (s1 /. i)),(1. L)%> by ;
len s1 = card (support b1) by ;
then i in dom s1 by ;
then ( s1 . i = s1 /. i & s1 . i in rng s1 ) by ;
then s1 /. i in support b1 by ;
then A40: s1 /. i in support (b1 + b2) by ;
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 ;
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 ;
A45: l in dom f by ;
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 ;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom () & (f . l) . 1 = () . ((Sum (Card (f | (l -' 1)))) + 1) ) by ;
then (f . l) . 1 in rng () by FUNCT_1:3;
hence contradiction by A32, A35, A38, A39, A43, A46, A44, A47, Def9; :: thesis: verum
end;
suppose x in rng () ; :: thesis: contradiction
then consider k being Nat such that
A48: k in dom () 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 = () . k by ;
f2 . i = fpoly_mult_root ((s2 /. i),(b2 . (s2 /. i))) by ;
then A53: (f2 . i) . j = <%(- (s2 /. i)),(1. L)%> by ;
len s2 = card (support b2) by ;
then i in dom s2 by ;
then ( s2 . i = s2 /. i & s2 . i in rng s2 ) by ;
then s2 /. i in support b2 by ;
then A54: s2 /. i in support (b1 + b2) by ;
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 ;
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 ;
A59: l in dom f by ;
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 ;
then ( (Sum (Card (f | (l -' 1)))) + 1 in dom () & (f . l) . 1 = () . ((Sum (Card (f | (l -' 1)))) + 1) ) by ;
then (f . l) . 1 in rng () by FUNCT_1:3;
hence contradiction by A32, A49, A52, A53, A57, A60, A58, A61, Def9; :: thesis: verum
end;
end;
end;
then ((FlattenSeq f1) ^ ()) " {x} = {} by FUNCT_1:72;
hence card (Coim ((),x)) = card (Coim ((() ^ ()),x)) by ; :: thesis: verum
end;
end;
end;
then FlattenSeq f,() ^ () are_fiberwise_equipotent by CLASSES1:def 10;
then ex p being Permutation of (dom ()) st FlattenSeq f = (() ^ ()) * p by ;
hence poly_with_roots (b1 + b2) = Product (() ^ ()) by
.= (Product ()) * (Product ()) by GROUP_4:5
.= () *' () by ;
:: thesis: verum