let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
let b be bag of ; :: thesis:
let f be FinSequence of the carrier of (Polynom-Ring L) * ; :: thesis:
let s be FinSequence of L; :: thesis:
let c be Element of L; :: thesis:
assume that
A1: len f = card (support b) and
A2: s = canFS (support b) and
A3: for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) ; :: thesis:
A4: len f = len s by A1, A2, Def1;
then A5: dom f = dom s by FINSEQ_3:31;

hereby :: thesis:

assume c in support b ; :: thesis:
then c in rng s by A2, FUNCT_2:def 3;
then consider i being Nat such that
A7: i in dom s and
A8: s . i = c by FINSEQ_2:11;
A9: s /. i = c by A7, A8, PARTFUN1:def 8;
A11: b . c = { k where k is Element of NAT : k < b . c } by AXIOMS:30;
set ff = FlattenSeq f;
set Y = (FlattenSeq f) " {<%(- c),(1. L)%>};
set X = { k where k is Element of NAT : k < b . c } ;
defpred S₁[ set , set ] means ex n being Element of NAT st
( n = $1 & $2 = (Sum (Card (f | (i -' 1)))) + (1 + n) );
A13: for x being set st x in { k where k is Element of NAT : k < b . c } holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis:
assume x in { k where k is Element of NAT : k < b . c } ; :: thesis:
then consider k being Element of NAT such that
A14: x = k and
k < b . c ;
take y = (Sum (Card (f | (i -' 1)))) + (1 + k); :: thesis:
thus S₁[x,y] by A14; :: thesis:

end;

consider g being Function such that
A15: dom g = { k where k is Element of NAT : k < b . c } and
A16: for x being set st x in { k where k is Element of NAT : k < b . c } holds
S₁[x,g . x] from CLASSES1:sch 1(A13);
A17: g is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A18: x1 in dom g and
A19: x2 in dom g and
A20: g . x1 = g . x2 ; :: thesis:
consider n1 being Element of NAT such that
A21: n1 = x1 and
A22: g . x1 = (Sum (Card (f | (i -' 1)))) + (1 + n1) by A15, A16, A18;
consider n2 being Element of NAT such that
A23: n2 = x2 and
A24: g . x2 = (Sum (Card (f | (i -' 1)))) + (1 + n2) by A15, A16, A19;
thus x1 = x2 by A20, A21, A22, A23, A24; :: thesis:

end;

now

let y be set ; :: thesis:

hereby :: thesis:

assume y in rng g ; :: thesis:
then consider x being set such that
A25: x in dom g and
A26: y = g . x by FUNCT_1:def 5;
consider k being Element of NAT such that
A27: x = k and
A28: k < b . c by A15, A25;
consider n being Element of NAT such that
A29: n = x and
A30: g . x = (Sum (Card (f | (i -' 1)))) + (1 + n) by A15, A16, A25;
A31: f . i = fpoly_mult_root (s /. i),(b . (s /. i)) by A3, A5, A7;
A32: ( 1 <= 1 + n & 1 + n <= b . c ) by A27, A28, A29, NAT_1:12, NAT_1:13;
len (f . i) = b . c by A9, A31, Def10;
then A33: 1 + n in dom (f . i) by A32, FINSEQ_3:27;
then A34: ( (Sum (Card (f | (i -' 1)))) + (1 + n) in dom (FlattenSeq f) & (f . i) . (1 + n) = (FlattenSeq f) . ((Sum (Card (f | (i -' 1)))) + (1 + n)) ) by A5, A7, POLYNOM1:33;
(f . i) . (1 + n) = <%(- c),(1. L)%> by A9, A31, A33, Def10;
then (f . i) . (1 + n) in {<%(- c),(1. L)%>} by TARSKI:def 1;
hence y in (FlattenSeq f) " {<%(- c),(1. L)%>} by A26, A30, A34, FUNCT_1:def 13; :: thesis:

end;

assume A35: y in (FlattenSeq f) " {<%(- c),(1. L)%>} ; :: thesis:
then A36: ( y in dom (FlattenSeq f) & (FlattenSeq f) . y in {<%(- c),(1. L)%>} ) by FUNCT_1:def 13;
reconsider yn = y as Element of NAT by A35;
consider i1, j being Element of NAT such that
A37: i1 in dom f and
A38: j in dom (f . i1) and
A39: yn = (Sum (Card (f | (i1 -' 1)))) + j and
A40: (f . i1) . j = (FlattenSeq f) . yn by A36, POLYNOM1:32;
consider j1 being Nat such that
A41: j = j1 + 1 by A38, FINSEQ_3:26, NAT_1:6;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
A42: f . i1 = fpoly_mult_root (s /. i1),(b . (s /. i1)) by A3, A37;
then (f . i1) . j = <%(- (s /. i1)),(1. L)%> by A38, Def10;
then A43: <%(- c),(1. L)%> = <%(- (s /. i1)),(1. L)%> by A36, A40, TARSKI:def 1;
( <%(- c),(1. L)%> . 0 = - c & <%(- (s /. i1)),(1. L)%> . 0 = - (s /. i1) ) by POLYNOM5:39;
then A44: c = s /. i1 by A43, RLVECT_1:31;
A45: i1 in dom s by A4, A37, FINSEQ_3:31;
s /. i1 = s . i1 by A5, A37, PARTFUN1:def 8;
then A46: i1 = i by A2, A7, A8, A44, A45, FUNCT_1:def 8;
len (f . i1) = b . c by A42, A44, Def10;
then j <= b . c by A38, FINSEQ_3:27;
then j1 < b . c by A41, NAT_1:13;
then A47: j1 in { k where k is Element of NAT : k < b . c } ;
then consider n being Element of NAT such that
A48: n = j1 and
A49: g . j1 = (Sum (Card (f | (i -' 1)))) + (1 + n) by A16;
thus y in rng g by A15, A39, A41, A46, A47, A48, A49, FUNCT_1:12; :: thesis:

end;

then rng g = (FlattenSeq f) " {<%(- c),(1. L)%>} by TARSKI:2;
then { k where k is Element of NAT : k < b . c } ,(FlattenSeq f) " {<%(- c),(1. L)%>} are_equipotent by A15, A17, WELLORD2:def 4;
hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by A11, CARD_1:def 5; :: thesis:

end;

assume that
A50: not c in support b and
A51: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0 ; :: thesis:
consider x being set such that
A52: x in (FlattenSeq f) " {<%(- c),(1. L)%>} by A51, CARD_1:47, XBOOLE_0:def 1;
A53: x in dom (FlattenSeq f) by A52, FUNCT_1:def 13;
reconsider x = x as Element of NAT by A52;
consider i, j being Element of NAT such that
A54: i in dom f and
A55: j in dom (f . i) and
x = (Sum (Card (f | (i -' 1)))) + j and
A56: (f . i) . j = (FlattenSeq f) . x by A53, POLYNOM1:32;
(FlattenSeq f) . x in {<%(- c),(1. L)%>} by A52, FUNCT_1:def 13;
then A57: (FlattenSeq f) . x = <%(- c),(1. L)%> by TARSKI:def 1;
f . i = fpoly_mult_root (s /. i),(b . (s /. i)) by A3, A54;
then A58: (f . i) . j = <%(- (s /. i)),(1. L)%> by A55, Def10;
( <%(- c),(1. L)%> . 0 = - c & <%(- (s /. i)),(1. L)%> . 0 = - (s /. i) ) by POLYNOM5:39;
then A59: c = s /. i by A56, A57, A58, RLVECT_1:31;
( s /. i = s . i & s . i in rng s ) by A5, A54, FUNCT_1:12, PARTFUN1:def 8;
hence contradiction by A2, A50, A59, FUNCT_2:def 3; :: thesis: