let n be Ordinal; :: thesis: for L being non trivial ZeroStr
for p being non-zero finite-Support Series of n,L ex b being bag of n st
( p . b <> 0. L & ( for b' being bag of n st b < b' holds
p . b' = 0. L ) )
let L be non trivial ZeroStr ; :: thesis: for p being non-zero finite-Support Series of n,L ex b being bag of n st
( p . b <> 0. L & ( for b' being bag of n st b < b' holds
p . b' = 0. L ) )
let p be non-zero finite-Support Series of n,L; :: thesis: ex b being bag of n st
( p . b <> 0. L & ( for b' being bag of n st b < b' holds
p . b' = 0. L ) )
defpred S₁[ Nat] means for B being finite Subset of st card B = $1 holds
ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) );
A1: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume A2: 1 <= k ; :: thesis: ( not S₁[k] or S₁[k + 1] )
thus ( S₁[k] implies S₁[k + 1] ) :: thesis: verum

proof

assume A3: S₁[k] ; :: thesis: S₁[k + 1]
thus S₁[k + 1] :: thesis: verum

proof

let B be finite Subset of ; :: thesis: ( card B = k + 1 implies ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) ) )
assume A4: card B = k + 1 ; :: thesis: ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) )
then reconsider B = B as non empty finite Subset of ;
consider x being Element of B;
x in B ;
then reconsider x = x as Element of Bags n ;
reconsider x = x as bag of n ;
set X = B \ {x};

now

let u be set ; :: thesis: ( u in {x} implies u in B )
assume u in {x} ; :: thesis: u in B
then u = x by TARSKI:def 1;
hence u in B ; :: thesis: verum

end;

then {x} c= B by TARSKI:def 3;
then A5: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ (B \ {x}) by XBOOLE_1:39 ;
( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def 5;
then A6: (card (B \ {x})) + 1 = k + 1 by A4, A5, CARD_2:54, TARSKI:def 1;
then reconsider X = B \ {x} as non empty set by A2, XCMPLX_1:2;
reconsider X = X as non empty finite Subset of ;
consider b being bag of n such that
A7: b in X and
A8: for b' being bag of n st b' in X holds
b' <=' b by A3, A6, XCMPLX_1:2;

A9: now

per cases ( x <=' b or b <=' x ) by PRE_POLY:45;

case A10: x <=' b ; :: thesis: for b' being bag of n st b' in B holds
b' <=' b

now

let b' be bag of n; :: thesis: ( b' in B implies b' <=' b )
assume A11: b' in B ; :: thesis: b' <=' b

now

per cases ( b' in X or not b' in X ) ;

case b' in X ; :: thesis: b' <=' b

hence b' <=' b by A8; :: thesis: verum

end;

case not b' in X ; :: thesis: b' <=' b

then b' in {x} by A5, A11, XBOOLE_0:def 3;
hence b' <=' b by A10, TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence b' <=' b ; :: thesis: verum

end;

hence for b' being bag of n st b' in B holds
b' <=' b ; :: thesis: verum

end;

case A12: b <=' x ; :: thesis: for b' being bag of n st b' in B holds
b' <=' x

now

let b' be bag of n; :: thesis: ( b' in B implies b' <=' x )
assume A13: b' in B ; :: thesis: b' <=' x

now

per cases ( b' in X or not b' in X ) ;

case b' in X ; :: thesis: b' <=' x

then b' <=' b by A8;
hence b' <=' x by A12, PRE_POLY:42; :: thesis: verum

end;

case not b' in X ; :: thesis: b' <=' x

then b' in {x} by A5, A13, XBOOLE_0:def 3;
hence b' <=' x by TARSKI:def 1; :: thesis: verum

end;

end;

end;

hence b' <=' x ; :: thesis: verum

end;

hence for b' being bag of n st b' in B holds
b' <=' x ; :: thesis: verum

end;

end;

end;

b in B by A5, A7, XBOOLE_0:def 3;
hence ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) ) by A9; :: thesis: verum

end;

thus verum ; :: thesis: verum

end;

end;

reconsider sp = Support p as finite set by POLYNOM1:def 10;
A14: Support p is finite Subset of by POLYNOM1:def 10;
card sp is finite ;
then consider m being Nat such that
A15: card (Support p) = card m by CARD_1:86;
p <> 0_ n,L by POLYNOM7:def 2;
then Support p <> {} by POLYNOM7:1;
then m <> 0 by A15;
then A16: 1 <= m by NAT_1:14;
A17: card (Support p) = m by A15, CARD_1:def 5;
A18: S₁[1]

proof

let B be finite Subset of ; :: thesis: ( card B = 1 implies ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) ) )
assume card B = 1 ; :: thesis: ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) )
then card {{} } = card B by CARD_1:50;
then consider b being set such that
A19: B = {b} by CARD_1:49;
A20: b in B by A19, TARSKI:def 1;
then reconsider b = b as Element of Bags n ;
reconsider b = b as bag of n ;
for b' being bag of n st b' in B holds
b' <=' b by A19, TARSKI:def 1;
hence ex b being bag of n st
( b in B & ( for b' being bag of n st b' in B holds
b' <=' b ) ) by A20; :: thesis: verum

end;

for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A18, A1);
then consider b being bag of n such that
A21: b in Support p and
A22: for b' being bag of n st b' in Support p holds
b' <=' b by A17, A16, A14;

A23: now

let b' be bag of n; :: thesis: ( b < b' implies p . b' = 0. L )
assume b < b' ; :: thesis: p . b' = 0. L
then not b' <=' b by Lm4;
then A24: not b' in Support p by A22;
b' is Element of Bags n by PRE_POLY:def 12;
hence p . b' = 0. L by A24, POLYNOM1:def 9; :: thesis: verum

end;

p . b <> 0. L by A21, POLYNOM1:def 9;
hence ex b being bag of n st
( p . b <> 0. L & ( for b' being bag of n st b < b' holds
p . b' = 0. L ) ) by A23; :: thesis: verum