let F be Field; :: thesis:
let m be Ordinal; :: thesis:
assume AS: m in card (nonConstantPolys F) ; :: thesis:
let p be non constant Polynomial of F; :: thesis:
set n = card (nonConstantPolys F);
set q = Poly (m,p);
for o being object st o in {m} holds
o in card (nonConstantPolys F) by AS, TARSKI:def 1;
then reconsider S = {m} as finite Subset of (card (nonConstantPolys F)) by TARSKI:def 3;
reconsider degp = deg p as non zero Element of NAT by RATFUNC1:def 2;
H: m in {m} by TARSKI:def 1;
K: deg p = (len p) - 1 by HURWITZ:def 2;
then I: deg p = (len p) -' 1 by XREAL_0:def 2;
set b = (S,degp) -bag ;
D: support ((S,degp) -bag) = S by UPROOTS:8;
E: (S,degp) -bag in Support (Poly (m,p))

proof

F: (Poly (m,p)) . ((S,degp) -bag) = p . (((S,degp) -bag) . m) by D, defPg
.= p . degp by H, UPROOTS:7 ;
p . degp = LC p by I, RATFUNC1:def 6;
then p . degp <> 0. F ;
hence (S,degp) -bag in Support (Poly (m,p)) by F, POLYNOM1:def 4; :: thesis:

end;

for b1 being bag of card (nonConstantPolys F) st b1 in Support (Poly (m,p)) holds
b1 <=' (S,degp) -bag

proof

let b1 be bag of card (nonConstantPolys F); :: thesis:
assume b1 in Support (Poly (m,p)) ; :: thesis:
then E1: (Poly (m,p)) . b1 <> 0. F by POLYNOM1:def 4;

per cases ;

suppose support b1 = {} ; :: thesis:

then b1 = EmptyBag (card (nonConstantPolys F)) by PRE_POLY:81;
hence b1 <=' (S,degp) -bag by PRE_POLY:60; :: thesis:

end;

suppose E0: support b1 = {m} ; :: thesis:

per cases ;

suppose b1 = (S,degp) -bag ; :: thesis:

hence b1 <=' (S,degp) -bag ; :: thesis:

end;

suppose EE: b1 <> (S,degp) -bag ; :: thesis:

E4: (Poly (m,p)) . b1 = p . (b1 . m) by E0, defPg;
E3: ((S,degp) -bag) . m = (len p) - 1 by K, H, UPROOTS:7;

E7: now :: thesis:

assume b1 . m >= ((S,degp) -bag) . m ; :: thesis:

per cases by XXREAL_0:1;

suppose E5: b1 . m = ((S,degp) -bag) . m ; :: thesis:

now :: thesis:

let i be object ; :: thesis:
assume i in card (nonConstantPolys F) ; :: thesis:

per cases ;

suppose i = m ; :: thesis:

hence b1 . i = ((S,degp) -bag) . i by E5; :: thesis:

end;

suppose i <> m ; :: thesis:

then E6: not i in {m} by TARSKI:def 1;
hence ((S,degp) -bag) . i = 0 by UPROOTS:6
.= b1 . i by E6, E0, PRE_POLY:def 7 ;
:: thesis:

end;

end;

end;

hence contradiction by EE, PBOOLE:def 10; :: thesis:

end;

suppose b1 . m > ((S,degp) -bag) . m ; :: thesis:

then b1 . m >= ((len p) - 1) + 1 by E3, INT_1:7;
hence contradiction by E4, E1, ALGSEQ_1:8; :: thesis:

end;

end;

end;

ex k being Ordinal st
( b1 . k < ((S,degp) -bag) . k & ( for l being Ordinal st l in k holds
b1 . l = ((S,degp) -bag) . l ) )

proof

take k = m; :: thesis:
thus b1 . k < ((S,degp) -bag) . k by E7; :: thesis:

now :: thesis:

let l be Ordinal; :: thesis:
assume l in k ; :: thesis:
then l <> k ;
then E8: not l in {m} by TARSKI:def 1;
hence ((S,degp) -bag) . l = 0 by UPROOTS:6
.= b1 . l by E8, E0, PRE_POLY:def 7 ;
:: thesis:

end;

hence for l being Ordinal st l in k holds
b1 . l = ((S,degp) -bag) . l ; :: thesis:

end;

hence b1 <=' (S,degp) -bag by PRE_POLY:def 9, PRE_POLY:def 10; :: thesis:

end;

end;

end;

suppose ( support b1 <> {} & support b1 <> {m} ) ; :: thesis:

hence b1 <=' (S,degp) -bag by E1, defPg; :: thesis:

end;

end;

end;

then F: (S,degp) -bag = Lt (Poly (m,p)) by E, LT1;
hence (Lt (Poly (m,p))) . m = deg p by H, UPROOTS:7; :: thesis:

now :: thesis:

let o be Ordinal; :: thesis:
assume o <> m ; :: thesis:
then not o in {m} by TARSKI:def 1;
hence (Lt (Poly (m,p))) . o = 0 by F, UPROOTS:6; :: thesis:

end;

hence for o being Ordinal st o <> m holds
(Lt (Poly (m,p))) . o = 0 ; :: thesis: