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 () *
for s being FinSequence of L
for c being Element of L st len f = card () & s = canFS () & ( 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )

let b be bag of the carrier of L; :: thesis: for f being FinSequence of the carrier of () *
for s being FinSequence of L
for c being Element of L st len f = card () & s = canFS () & ( 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )

let f be FinSequence of the carrier of () * ; :: thesis: for s being FinSequence of L
for c being Element of L st len f = card () & s = canFS () & ( 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )

let s be FinSequence of L; :: thesis: for c being Element of L st len f = card () & s = canFS () & ( 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )

let c be Element of L; :: thesis: ( len f = card () & s = canFS () & ( 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) ) )

assume that
A1: len f = card () and
A2: s = canFS () 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 (() " {<%(- c),(1. L)%>}) = b . c ) & ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 ) )
len f = len s by ;
then A4: dom f = dom s by FINSEQ_3:29;
hereby :: thesis: ( not c in support b implies card (() " {<%(- c),(1. L)%>}) = 0 )
set X = { k where k is Nat : k < b . c } ;
set ff = FlattenSeq f;
set Y = () " {<%(- c),(1. L)%>};
assume c in support b ; :: thesis: card (() " {<%(- c),(1. L)%>}) = b . c
then c in rng s by ;
then consider i being Nat such that
A5: i in dom s and
A6: s . i = c by FINSEQ_2:10;
defpred S1[ 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 S1[x,y]
proof
let x be object ; :: thesis: ( x in { k where k is Nat : k < b . c } implies ex y being object st S1[x,y] )
assume x in { k where k is Nat : k < b . c } ; :: thesis: ex y being object st S1[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: S1[x,(Sum (Card (f | (i -' 1)))) + (1 + k)]
thus S1[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
S1[x,g . x] from A11: s /. i = c by ;
now :: thesis: for y being object holds
( ( y in rng g implies y in () " {<%(- c),(1. L)%>} ) & ( y in () " {<%(- c),(1. L)%>} implies y in rng g ) )
let y be object ; :: thesis: ( ( y in rng g implies y in () " {<%(- c),(1. L)%>} ) & ( y in () " {<%(- c),(1. L)%>} implies y in rng g ) )
A12: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;
hereby :: thesis: ( y in () " {<%(- c),(1. L)%>} implies y in rng g )
assume y in rng g ; :: thesis: y in () " {<%(- 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 ;
then A17: ( 1 <= 1 + n & 1 + n <= b . c ) by ;
A18: f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by A3, A4, A5;
then len (f . i) = b . c by ;
then A19: 1 + n in dom (f . i) by ;
then (f . i) . (1 + n) = <%(- c),(1. L)%> by ;
then A20: (f . i) . (1 + n) in {<%(- c),(1. L)%>} by TARSKI:def 1;
( (Sum (Card (f | (i -' 1)))) + (1 + n) in dom () & (f . i) . (1 + n) = () . ((Sum (Card (f | (i -' 1)))) + (1 + n)) ) by ;
hence y in () " {<%(- c),(1. L)%>} by ; :: thesis: verum
end;
assume A21: y in () " {<%(- 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 ;
y in dom () by ;
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 = () . yn by PRE_POLY:29;
A27: f . i1 = fpoly_mult_root ((s /. i1),(b . (s /. i1))) by ;
then (f . i1) . j = <%(- (s /. i1)),(1. L)%> by ;
then <%(- c),(1. L)%> = <%(- (s /. i1)),(1. L)%> by ;
then A28: c = s /. i1 by ;
( i1 in dom s & s /. i1 = s . i1 ) by ;
then A29: i1 = i by ;
consider j1 being Nat such that
A30: j = j1 + 1 by ;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 12;
len (f . i1) = b . c by ;
then j <= b . c by ;
then j1 < b . c by ;
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 ; :: thesis: verum
end;
then A32: rng g = () " {<%(- 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 } ,() " {<%(- c),(1. L)%>} are_equipotent ) by ;
hence card (() " {<%(- c),(1. L)%>}) = b . c by CARD_1:def 2; :: thesis: verum
end;
assume that
A35: not c in support b and
A36: card (() " {<%(- c),(1. L)%>}) <> 0 ; :: thesis: contradiction
consider x being object such that
A37: x in () " {<%(- c),(1. L)%>} by ;
A38: x in dom () by ;
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 = () . x by ;
A42: ( s /. i = s . i & s . i in rng s ) by ;
(FlattenSeq f) . x in {<%(- c),(1. L)%>} by ;
then A43: (FlattenSeq f) . x = <%(- c),(1. L)%> by TARSKI:def 1;
f . i = fpoly_mult_root ((s /. i),(b . (s /. i))) by ;
then A44: (f . i) . j = <%(- (s /. i)),(1. L)%> by ;
<%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;
then c = s /. i by ;
hence contradiction by A2, A35, A42, FUNCT_2:def 3; :: thesis: verum