let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: for b being bag of the carrier of L
for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let b be bag of the carrier of L; :: thesis: for f being FinSequence of the carrier of (Polynom-Ring L) *
for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let f be FinSequence of the carrier of (Polynom-Ring L) * ; :: thesis: for s being FinSequence of L
for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let s be FinSequence of L; :: thesis: for c being Element of L st len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) holds
( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
let c be Element of L; :: thesis: ( len f = card (support b) & s = canFS (support b) & ( for i being Element of NAT st i in dom f holds
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) ) implies ( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) ) )
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: ( ( c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 ) )
len f = len s by A1, A2, FINSEQ_1:93;
then A4: dom f = dom s by FINSEQ_3:29;

hereby :: thesis: ( not c in support b implies card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = 0 )

set X = { k where k is Nat : k < b . c } ;
set ff = FlattenSeq f;
set Y = (FlattenSeq f) " {<%(- c),(1. L)%>};
assume c in support b ; :: thesis: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c
then c in rng s by A2, FUNCT_2:def 3;
then consider i being Nat such that
A5: i in dom s and
A6: s . i = c by FINSEQ_2:10;
defpred S₁[ object , object ] means ex n being Nat st
( n = $1 & $2 = (Sum (Card (f | (i -' 1)))) + (1 + n) );
A7: for x being object st x in { k where k is Nat : k < b . c } holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in { k where k is Nat : k < b . c } implies ex y being object st S₁[x,y] )
assume x in { k where k is Nat : k < b . c } ; :: thesis: ex y being object st S₁[x,y]
then consider k being Nat such that
A8: x = k and
k < b . c ;
take (Sum (Card (f | (i -' 1)))) + (1 + k) ; :: thesis: S₁[x,(Sum (Card (f | (i -' 1)))) + (1 + k)]
thus S₁[x,(Sum (Card (f | (i -' 1)))) + (1 + k)] by A8; :: thesis: verum

end;

consider g being Function such that
A9: dom g = { k where k is Nat : k < b . c } and
A10: for x being object st x in { k where k is Nat : k < b . c } holds
S₁[x,g . x] from CLASSES1:sch 1(A7);
A11: s /. i = c by A5, A6, PARTFUN1:def 6;

now :: thesis: for y being object holds
( ( y in rng g implies y in (FlattenSeq f) " {<%(- c),(1. L)%>} ) & ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g ) )

let y be object ; :: thesis: ( ( y in rng g implies y in (FlattenSeq f) " {<%(- c),(1. L)%>} ) & ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g ) )
A12: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;

hereby :: thesis: ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g )

assume y in rng g ; :: thesis: y in (FlattenSeq f) " {<%(- c),(1. L)%>}
then consider x being object such that
A13: x in dom g and
A14: y = g . x by FUNCT_1:def 3;
consider n being Nat such that
A15: n = x and
A16: g . x = (Sum (Card (f | (i -' 1)))) + (1 + n) by A9, A10, A13;
ex k being Nat st
( x = k & k < b . c ) by A9, A13;
then A17: ( 1 <= 1 + n & 1 + n <= b . c ) by A15, NAT_1:12, NAT_1:13;
A18: f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A4, A5;
then len (f . i) = b . c by A11, Def9;
then A19: 1 + n in dom (f . i) by A17, FINSEQ_3:25;
then (f . i) . (1 + n) = <%(- c),(1. L)%> by A11, A18, Def9;
then A20: (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 A4, A5, A19, PRE_POLY:30;
hence y in (FlattenSeq f) " {<%(- c),(1. L)%>} by A14, A16, A20, FUNCT_1:def 7; :: thesis: verum

end;

assume A21: y in (FlattenSeq f) " {<%(- c),(1. L)%>} ; :: thesis: y in rng g
then reconsider yn = y as Element of NAT ;
A22: (FlattenSeq f) . y in {<%(- c),(1. L)%>} by A21, FUNCT_1:def 7;
y in dom (FlattenSeq f) by A21, FUNCT_1:def 7;
then consider i1, j being Nat such that
A23: i1 in dom f and
A24: j in dom (f . i1) and
A25: yn = (Sum (Card (f | (i1 -' 1)))) + j and
A26: (f . i1) . j = (FlattenSeq f) . yn by PRE_POLY:29;
A27: f . i1 = fpoly_mult_root ((s /. i1),(b . (s /. i1))) by A3, A23;
then (f . i1) . j = <%(- (s /. i1)),(1. L)%> by A24, Def9;
then <%(- c),(1. L)%> = <%(- (s /. i1)),(1. L)%> by A22, A26, TARSKI:def 1;
then A28: c = s /. i1 by A12, POLYNOM5:38, RLVECT_1:18;
( i1 in dom s & s /. i1 = s . i1 ) by A4, A23, PARTFUN1:def 6;
then A29: i1 = i by A2, A5, A6, A28, FUNCT_1:def 4;
consider j1 being Nat such that
A30: j = j1 + 1 by A24, FINSEQ_3:24, NAT_1:6;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 12;
len (f . i1) = b . c by A27, A28, Def9;
then j <= b . c by A24, FINSEQ_3:25;
then j1 < b . c by A30, NAT_1:13;
then A31: j1 in { k where k is Nat : k < b . c } ;
then ex n being Nat st
( n = j1 & g . j1 = (Sum (Card (f | (i -' 1)))) + (1 + n) ) by A10;
hence y in rng g by A9, A25, A30, A29, A31, FUNCT_1:3; :: thesis: verum

end;

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

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 g or not x2 in proj1 g or not g . x1 = g . x2 or x1 = x2 )
assume that
A33: ( x1 in dom g & x2 in dom g ) and
A34: g . x1 = g . x2 ; :: thesis: x1 = x2
( ex n1 being Nat st
( n1 = x1 & g . x1 = (Sum (Card (f | (i -' 1)))) + (1 + n1) ) & ex n2 being Nat st
( n2 = x2 & g . x2 = (Sum (Card (f | (i -' 1)))) + (1 + n2) ) ) by A9, A10, A33;
hence x1 = x2 by A34; :: thesis: verum

end;

then ( b . c = { k where k is Nat : k < b . c } & { k where k is Nat : k < b . c } ,(FlattenSeq f) " {<%(- c),(1. L)%>} are_equipotent ) by A9, A32, AXIOMS:4, WELLORD2:def 4;
hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def 2; :: thesis: verum

end;

assume that
A35: not c in support b and
A36: card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0 ; :: thesis: contradiction
consider x being object such that
A37: x in (FlattenSeq f) " {<%(- c),(1. L)%>} by A36, CARD_1:27, XBOOLE_0:def 1;
A38: x in dom (FlattenSeq f) by A37, FUNCT_1:def 7;
reconsider x = x as Element of NAT by A37;
consider i, j being Nat such that
A39: i in dom f and
A40: j in dom (f . i) and
x = (Sum (Card (f | (i -' 1)))) + j and
A41: (f . i) . j = (FlattenSeq f) . x by A38, PRE_POLY:29;
A42: ( s /. i = s . i & s . i in rng s ) by A4, A39, FUNCT_1:3, PARTFUN1:def 6;
(FlattenSeq f) . x in {<%(- c),(1. L)%>} by A37, FUNCT_1:def 7;
then A43: (FlattenSeq f) . x = <%(- c),(1. L)%> by TARSKI:def 1;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A39;
then A44: (f . i) . j = <%(- (s /. i)),(1. L)%> by A40, Def9;
<%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;
then c = s /. i by A41, A43, A44, POLYNOM5:38, RLVECT_1:18;
hence contradiction by A2, A35, A42, FUNCT_2:def 3; :: thesis: verum