let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; 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; 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) * ; 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; 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; ( 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)))
; ( ( 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 ( 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
;
card ((FlattenSeq f) " {<%(- c),(1. L)%>}) = b . cthen
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 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]
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 CLASSES1:sch 1(A7);
A11:
s /. i = c
by A5, A6, PARTFUN1:def 6;
now 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 ;
( ( 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 ( y in (FlattenSeq f) " {<%(- c),(1. L)%>} implies y in rng g )
assume
y in rng g
;
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;
verum
end; assume A21:
y in (FlattenSeq f) " {<%(- c),(1. L)%>}
;
y in rng gthen 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;
verum end; then A32:
rng g = (FlattenSeq f) " {<%(- c),(1. L)%>}
by TARSKI:2;
g is
one-to-one
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;
verum
end;
assume that
A35:
not c in support b
and
A36:
card ((FlattenSeq f) " {<%(- c),(1. L)%>}) <> 0
; 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; verum