let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis:
let b be bag of the carrier of L; :: 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:
len f = len s by A1, A2, Th5;
then A5: dom f = dom s by FINSEQ_3:31;

hereby :: thesis:

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

end;

consider g being Function such that
A10: dom g = { k where k is Element of NAT : k < b . c } and
A11: 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(A8);
A12: s /. i = c by A6, A7, PARTFUN1:def 8;

now

let y be set ; :: thesis:
A13: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:39;

hereby :: thesis:

assume y in rng g ; :: thesis:
then consider x being set such that
A14: x in dom g and
A15: y = g . x by FUNCT_1:def 5;
consider n being Element of NAT such that
A16: n = x and
A17: g . x = (Sum (Card (f | (i -' 1)))) + (1 + n) by A10, A11, A14;
ex k being Element of NAT st
( x = k & k < b . c ) by A10, A14;
then A18: ( 1 <= 1 + n & 1 + n <= b . c ) by A16, NAT_1:12, NAT_1:13;
A19: f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A5, A6;
then len (f . i) = b . c by A12, Def10;
then A20: 1 + n in dom (f . i) by A18, FINSEQ_3:27;
then (f . i) . (1 + n) = <%(- c),(1. L)%> by A12, A19, Def10;
then A21: (f . i) . (1 + n) in {<%(- c),(1. L)%>} by TARSKI:def 1;
( (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, A6, A20, PRE_POLY:30;
hence y in (FlattenSeq f) " {<%(- c),(1. L)%>} by A15, A17, A21, FUNCT_1:def 13; :: thesis:

end;

assume A22: y in (FlattenSeq f) " {<%(- c),(1. L)%>} ; :: thesis:
then reconsider yn = y as Element of NAT ;
A23: (FlattenSeq f) . y in {<%(- c),(1. L)%>} by A22, FUNCT_1:def 13;
y in dom (FlattenSeq f) by A22, FUNCT_1:def 13;
then consider i1, j being Element of NAT such that
A24: i1 in dom f and
A25: j in dom (f . i1) and
A26: yn = (Sum (Card (f | (i1 -' 1)))) + j and
A27: (f . i1) . j = (FlattenSeq f) . yn by PRE_POLY:29;
A28: f . i1 = fpoly_mult_root ((s /. i1),(b . (s /. i1))) by A3, A24;
then (f . i1) . j = <%(- (s /. i1)),(1. L)%> by A25, Def10;
then <%(- c),(1. L)%> = <%(- (s /. i1)),(1. L)%> by A23, A27, TARSKI:def 1;
then A29: c = s /. i1 by A13, POLYNOM5:39, RLVECT_1:31;
( i1 in dom s & s /. i1 = s . i1 ) by A5, A24, PARTFUN1:def 8;
then A30: i1 = i by A2, A6, A7, A29, FUNCT_1:def 8;
consider j1 being Nat such that
A31: j = j1 + 1 by A25, FINSEQ_3:26, NAT_1:6;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
len (f . i1) = b . c by A28, A29, Def10;
then j <= b . c by A25, FINSEQ_3:27;
then j1 < b . c by A31, NAT_1:13;
then A32: j1 in { k where k is Element of NAT : k < b . c } ;
then ex n being Element of NAT st
( n = j1 & g . j1 = (Sum (Card (f | (i -' 1)))) + (1 + n) ) by A11;
hence y in rng g by A10, A26, A31, A30, A32, FUNCT_1:12; :: thesis:

end;

then A33: rng g = (FlattenSeq f) " {<%(- c),(1. L)%>} by TARSKI:2;
g is one-to-one

proof

let x1, x2 be set ; :: according to FUNCT_1:def 8 :: thesis:
assume that
A34: ( x1 in dom g & x2 in dom g ) and
A35: g . x1 = g . x2 ; :: thesis:
( ex n1 being Element of NAT st
( n1 = x1 & g . x1 = (Sum (Card (f | (i -' 1)))) + (1 + n1) ) & ex n2 being Element of NAT st
( n2 = x2 & g . x2 = (Sum (Card (f | (i -' 1)))) + (1 + n2) ) ) by A10, A11, A34;
hence x1 = x2 by A35; :: thesis:

end;

then ( b . c = { k where k is Element of NAT : k < b . c } & { k where k is Element of NAT : k < b . c } ,(FlattenSeq f) " {<%(- c),(1. L)%>} are_equipotent ) by A10, A33, AXIOMS:30, WELLORD2:def 4;
hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def 5; :: thesis:

end;

assume that
A36: not c in support b and
A37: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0 ; :: thesis:
consider x being set such that
A38: x in (FlattenSeq f) " {<%(- c),(1. L)%>} by A37, CARD_1:47, XBOOLE_0:def 1;
A39: x in dom (FlattenSeq f) by A38, FUNCT_1:def 13;
reconsider x = x as Element of NAT by A38;
consider i, j being Element of NAT such that
A40: i in dom f and
A41: j in dom (f . i) and
x = (Sum (Card (f | (i -' 1)))) + j and
A42: (f . i) . j = (FlattenSeq f) . x by A39, PRE_POLY:29;
A43: ( s /. i = s . i & s . i in rng s ) by A5, A40, FUNCT_1:12, PARTFUN1:def 8;
(FlattenSeq f) . x in {<%(- c),(1. L)%>} by A38, FUNCT_1:def 13;
then A44: (FlattenSeq f) . x = <%(- c),(1. L)%> by TARSKI:def 1;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A40;
then A45: (f . i) . j = <%(- (s /. i)),(1. L)%> by A41, Def10;
<%(- c),(1. L)%> . 0 = - c by POLYNOM5:39;
then c = s /. i by A42, A44, A45, POLYNOM5:39, RLVECT_1:31;
hence contradiction by A2, A36, A43, FUNCT_2:def 3; :: thesis: