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

proof

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

proof

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

proof

let B be finite Subset of (Bags n); :: thesis:
assume A4: card B = k + 1 ; :: thesis:
then reconsider B = B as non empty finite Subset of (Bags n) ;
consider x being Element of B;
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:
assume u in {x} ; :: thesis:
then u = x by TARSKI:def 1;
hence u in B ; :: thesis:

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 (Bags n) ;
consider b being bag of n such that
A7: b in X and
A8: for b9 being bag of n st b9 in X holds
b9 <=' b by A3, A6, XCMPLX_1:2;

A9: now

per cases by PRE_POLY:45;

case A10: x <=' b ; :: thesis:

now

let b9 be bag of n; :: thesis:
assume A11: b9 in B ; :: thesis:

now

per cases ;

case b9 in X ; :: thesis:

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

end;

case not b9 in X ; :: thesis:

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

end;

end;

end;

hence b9 <=' b ; :: thesis:

end;

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

end;

case A12: b <=' x ; :: thesis:

now

let b9 be bag of n; :: thesis:
assume A13: b9 in B ; :: thesis:

now

per cases ;

case b9 in X ; :: thesis:

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

end;

case not b9 in X ; :: thesis:

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

end;

end;

end;

hence b9 <=' x ; :: thesis:

end;

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

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 b9 being bag of n st b9 in B holds
b9 <=' b ) ) by A9; :: thesis:

end;

end;

end;

reconsider sp = Support p as finite set by POLYNOM1:def 10;
A14: Support p is finite Subset of (Bags n) 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 (Bags n); :: thesis:
assume card B = 1 ; :: thesis:
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 b9 being bag of n st b9 in B holds
b9 <=' b by A19, TARSKI:def 1;
hence ex b being bag of n st
( b in B & ( for b9 being bag of n st b9 in B holds
b9 <=' b ) ) by A20; :: thesis:

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 b9 being bag of n st b9 in Support p holds
b9 <=' b by A17, A16, A14;

A23: now

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

end;

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