let F be Field; :: thesis: for n being Ordinal
for p being Monomial of n,F holds
( LC p = coefficient p & Lt p = term p )
let n be Ordinal; :: thesis: for p being Monomial of n,F holds
( LC p = coefficient p & Lt p = term p )
let p be Monomial of n,F; :: thesis: ( LC p = coefficient p & Lt p = term p )
H: ( Lt p is Element of Bags n & term p is Element of Bags n ) by PRE_POLY:def 12;
field (BagOrder n) = Bags n by ORDERS_1:12;
then A: BagOrder n linearly_orders Support p by ORDERS_1:37, ORDERS_1:38;

per cases ( p . (term p) <> 0. F or ( Support p = {} & term p = EmptyBag n ) ) by POLYNOM7:def 5;

suppose p . (term p) <> 0. F ; :: thesis: ( LC p = coefficient p & Lt p = term p )

then AS: term p in Support p by H, POLYNOM1:def 4;
then B: Support p = {(term p)} by POLYNOM7:7;
then C: rng (SgmX ((BagOrder n),(Support p))) = {(term p)} by A, PRE_POLY:def 2;
F: card (Support p) = 1 by B, CARD_1:30;
then D: len (SgmX ((BagOrder n),(Support p))) = 1 by A, PRE_POLY:11;
E: SgmX ((BagOrder n),(Support p)) = <*(term p)*> by F, C, A, PRE_POLY:11, FINSEQ_1:39;
p <> 0_ (n,F) by AS, YY;
then Lt p = (SgmX ((BagOrder n),(Support p))) . 1 by D, defLT
.= term p by E ;
hence ( LC p = coefficient p & Lt p = term p ) by POLYNOM7:def 6; :: thesis: verum

end;

suppose J: ( Support p = {} & term p = EmptyBag n ) ; :: thesis: ( LC p = coefficient p & Lt p = term p )

then K: LC p = 0. F by H, POLYNOM1:def 4;
then L: LC p = p . (term p) by J, POLYNOM1:def 4
.= coefficient p by POLYNOM7:def 6 ;
then p = Monom ((0. F),(term p)) by K, POLYNOM7:11;
then M: term p = EmptyBag n by POLYNOM7:8;
p = 0_ (n,F) by J, YY;
hence ( LC p = coefficient p & Lt p = term p ) by M, L, defLT; :: thesis: verum

end;

end;