let F be Field; :: thesis: for m being Ordinal st m in card (nonConstantPolys F) holds
for p being non constant Polynomial of F holds
( support (Lt (Poly (m,p))) = {m} & (Lt (Poly (m,p))) . m = deg p )
let m be Ordinal; :: thesis: ( m in card (nonConstantPolys F) implies for p being non constant Polynomial of F holds
( support (Lt (Poly (m,p))) = {m} & (Lt (Poly (m,p))) . m = deg p ) )
assume AS: m in card (nonConstantPolys F) ; :: thesis: for p being non constant Polynomial of F holds
( support (Lt (Poly (m,p))) = {m} & (Lt (Poly (m,p))) . m = deg p )
let p be non constant Polynomial of F; :: thesis: ( support (Lt (Poly (m,p))) = {m} & (Lt (Poly (m,p))) . m = deg p )
set n = card (nonConstantPolys F);
set q = Poly (m,p);

A: now :: thesis: for o being object st o in support (Lt (Poly (m,p))) holds
o in {m}

let o be object ; :: thesis: ( o in support (Lt (Poly (m,p))) implies o in {m} )
assume A1: o in support (Lt (Poly (m,p))) ; :: thesis: o in {m}
then reconsider i = o as Element of card (nonConstantPolys F) ;
(Lt (Poly (m,p))) . o <> 0 by A1, PRE_POLY:def 7;
then i = m by AS, XYZaa;
hence o in {m} by TARSKI:def 1; :: thesis: verum

end;

now :: thesis: for o being object st o in {m} holds
o in support (Lt (Poly (m,p)))

let o be object ; :: thesis: ( o in {m} implies o in support (Lt (Poly (m,p))) )
assume o in {m} ; :: thesis: o in support (Lt (Poly (m,p)))
then o = m by TARSKI:def 1;
then B1: (Lt (Poly (m,p))) . o = deg p by AS, XYZaa;
deg p > 0 by RATFUNC1:def 2;
hence o in support (Lt (Poly (m,p))) by B1, PRE_POLY:def 7; :: thesis: verum

end;

hence support (Lt (Poly (m,p))) = {m} by A, TARSKI:2; :: thesis: (Lt (Poly (m,p))) . m = deg p
thus (Lt (Poly (m,p))) . m = deg p by AS, XYZaa; :: thesis: verum