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;

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

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 )

assume that 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_{1}[ 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_{1}[x,y]

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_{1}[x,g . x]
from CLASSES1:sch 1(A7);

A11: s /. i = c by A5, A6, PARTFUN1:def 6;

g is one-to-one

hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def 2; :: thesis: verum

end;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

( 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

proof

consider g being Function such that
let x be object ; :: thesis: ( x in { k where k is Nat : k < b . c } implies ex y being object st S_{1}[x,y] )

assume x in { k where k is Nat : k < b . c } ; :: thesis: ex y being object st S_{1}[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_{1}[x,(Sum (Card (f | (i -' 1)))) + (1 + k)]

thus S_{1}[x,(Sum (Card (f | (i -' 1)))) + (1 + k)]
by A8; :: thesis: verum

end;assume x in { k where k is Nat : k < b . c } ; :: thesis: ex y being object st S

then consider k being Nat such that

A8: x = k and

k < b . c ;

take (Sum (Card (f | (i -' 1)))) + (1 + k) ; :: thesis: S

thus S

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

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 ) )

then A32:
rng g = (FlattenSeq f) " {<%(- c),(1. L)%>}
by TARSKI:2;( ( 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;

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;A12: <%(- c),(1. L)%> . 0 = - c by POLYNOM5:38;

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

assume A21:
y in (FlattenSeq f) " {<%(- c),(1. L)%>}
; :: thesis: y in rng gassume
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;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

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

g is one-to-one

proof

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;
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;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

hence card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . c by CARD_1:def 2; :: thesis: verum

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