let n be Ordinal; :: thesis:
let L be non trivial ZeroStr ; :: thesis:
let p be finite-Support non-zero Series of n,L; :: thesis:
p <> 0_ n,L by POLYNOM7:def 2;
then A1: Support p <> {} by POLYNOM7:1;
defpred S₁[ Nat] means for B being finite Subset of (Bags n) st card B = $1 holds
ex b being bag of st
( b in B & ( for b' being bag of st b' in B holds
b' <=' b ) );
A2: S₁[1]

proof

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

end;

A6: for k being Nat st 1 <= k & S₁[k] holds
S₁[k + 1]

proof

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

proof

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

proof

let B be finite Subset of (Bags n); :: thesis:
assume A9: card B = k + 1 ; :: thesis:
then reconsider B = B as non empty finite Subset of (Bags n) ;
consider x being Element of B;
( x in B & B c= Bags n ) ;
then reconsider x = x as Element of Bags n ;
reconsider x = x as bag of ;
set X = B \ {x};
A10: ( x in B \ {x} iff ( x in B & not x in {x} ) ) by XBOOLE_0:def 5;

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 A11: B = {x} \/ B by XBOOLE_1:12
.= {x} \/ (B \ {x}) by XBOOLE_1:39 ;
then A12: (card (B \ {x})) + 1 = k + 1 by A9, A10, CARD_2:54, TARSKI:def 1;
then A13: card (B \ {x}) = k by XCMPLX_1:2;
reconsider X = B \ {x} as non empty set by A7, A12, XCMPLX_1:2;
reconsider X = X as non empty finite Subset of (Bags n) ;
consider b being bag of such that
A14: ( b in X & ( for b' being bag of st b' in X holds
b' <=' b ) ) by A8, A13;

A15: now

per cases by POLYNOM1:49;

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

now

let b' be bag of ; :: thesis:
assume A17: b' in B ; :: thesis:

now

per cases ;

case b' in X ; :: thesis:

hence b' <=' b by A14; :: thesis:

end;

case not b' in X ; :: thesis:

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

end;

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

end;

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

end;

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

now

let b' be bag of ; :: thesis:
assume A19: b' in B ; :: thesis:

now

per cases ;

case b' in X ; :: thesis:

then b' <=' b by A14;
hence b' <=' x by A18, POLYNOM1:46; :: thesis:

end;

case not b' in X ; :: thesis:

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

end;

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

end;

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

end;

b in B by A11, A14, XBOOLE_0:def 3;
hence ex b being bag of st
( b in B & ( for b' being bag of st b' in B holds
b' <=' b ) ) by A15; :: thesis:

end;

thus verum ; :: thesis:

end;

A20: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(A2, A6);
reconsider sp = Support p as finite set by POLYNOM1:def 10;
card sp is finite ;
then consider m being Nat such that
A21: card (Support p) = card m by CARD_1:86;
A22: card (Support p) = m by A21, CARD_1:def 5;
m <> 0 by A21, A1;
then A23: 1 <= m by NAT_1:14;
Support p is finite Subset of (Bags n) by POLYNOM1:def 10;
then consider b being bag of such that
A24: ( b in Support p & ( for b' being bag of st b' in Support p holds
b' <=' b ) ) by A20, A22, A23;
A25: p . b <> 0. L by A24, POLYNOM1:def 9;

now

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

end;

hence ex b being bag of st
( p . b <> 0. L & ( for b' being bag of st b < b' holds
p . b' = 0. L ) ) by A25; :: thesis: