let R be non degenerated Ring; :: thesis: for n being Ordinal
for p being Polynomial of n,R
for b being bag of n st b in Support p holds
( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )
let n be Ordinal; :: thesis: for p being Polynomial of n,R
for b being bag of n st b in Support p holds
( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )
let p be Polynomial of n,R; :: thesis: for b being bag of n st b in Support p holds
( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )
let b be bag of n; :: thesis: ( b in Support p implies ( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b ) )
set F = SgmX ((BagOrder n),(Support p));
assume AS1: b in Support p ; :: thesis: ( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b )
then AS2: p <> 0_ (n,R) by YY;
field (BagOrder n) = Bags n by ORDERS_1:12;
then AS3: BagOrder n linearly_orders Support p by ORDERS_1:37, ORDERS_1:38;
card (Support p) >= 0 + 1 by AS1, INT_1:7;
then 1 <= len (SgmX ((BagOrder n),(Support p))) by AS3, PRE_POLY:11;
then len (SgmX ((BagOrder n),(Support p))) in Seg (len (SgmX ((BagOrder n),(Support p)))) ;
then AS4: len (SgmX ((BagOrder n),(Support p))) in dom (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:def 3;
then AS5: (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) = (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) by PARTFUN1:def 6;

A: now :: thesis: ( b = Lt p implies for b1 being bag of n st b1 in Support p holds
b1 <=' b )

assume AS6: b = Lt p ; :: thesis: for b1 being bag of n st b1 in Support p holds
b1 <=' b
then A0: b = (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) by AS2, defLT;
thus for b1 being bag of n st b1 in Support p holds
b1 <=' b :: thesis: verum

proof

let b1 be bag of n; :: thesis: ( b1 in Support p implies b1 <=' b )
assume b1 in Support p ; :: thesis: b1 <=' b
then b1 in rng (SgmX ((BagOrder n),(Support p))) by AS3, PRE_POLY:def 2;
then consider o being object such that
A1: ( o in dom (SgmX ((BagOrder n),(Support p))) & b1 = (SgmX ((BagOrder n),(Support p))) . o ) by FUNCT_1:def 3;
reconsider i = o as Element of NAT by A1;
A2: (SgmX ((BagOrder n),(Support p))) . i = (SgmX ((BagOrder n),(Support p))) /. i by A1, PARTFUN1:def 6;
i in Seg (len (SgmX ((BagOrder n),(Support p)))) by A1, FINSEQ_1:def 3;
then i <= len (SgmX ((BagOrder n),(Support p))) by FINSEQ_1:1;

per cases then ( i = len (SgmX ((BagOrder n),(Support p))) or i < len (SgmX ((BagOrder n),(Support p))) ) by XXREAL_0:1;

suppose i = len (SgmX ((BagOrder n),(Support p))) ; :: thesis: b1 <=' b

hence b1 <=' b by AS6, A1, AS2, defLT; :: thesis: verum

end;

suppose i < len (SgmX ((BagOrder n),(Support p))) ; :: thesis: b1 <=' b

then [b1,b] in BagOrder n by A0, A1, A2, AS4, AS5, AS3, PRE_POLY:def 2;
hence b1 <=' b by PRE_POLY:def 14; :: thesis: verum

end;

end;

end;

end;

now :: thesis: ( ( for b1 being bag of n st b1 in Support p holds
b1 <=' b ) implies b = Lt p )

assume B: for b1 being bag of n st b1 in Support p holds
b1 <=' b ; :: thesis: b = Lt p

now :: thesis: for y being Element of Bags n st y in Support p holds
[y,b] in BagOrder n

let y be Element of Bags n; :: thesis: ( y in Support p implies [y,b] in BagOrder n )
assume y in Support p ; :: thesis: [y,b] in BagOrder n
then y <=' b by B;
hence [y,b] in BagOrder n by PRE_POLY:def 14; :: thesis: verum

end;

then b = (SgmX ((BagOrder n),(Support p))) /. (len (SgmX ((BagOrder n),(Support p)))) by AS1, AS3, PRE_POLY:21
.= (SgmX ((BagOrder n),(Support p))) . (len (SgmX ((BagOrder n),(Support p)))) by AS4, PARTFUN1:def 6 ;
hence b = Lt p by AS2, defLT; :: thesis: verum

end;

hence ( b = Lt p iff for b1 being bag of n st b1 in Support p holds
b1 <=' b ) by A; :: thesis: verum