let n be Ordinal; :: thesis: for T being connected TermOrder of n

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let p be Polynomial of n,L; :: thesis: for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let j be Element of NAT ; :: thesis: ( j = (card (Support p)) - 1 implies Low (p,T,j) is non-zero Monomial of n,L )

set l = Low (p,T,j);

assume A1: j = (card (Support p)) - 1 ; :: thesis: Low (p,T,j) is non-zero Monomial of n,L

then card (Support (Low (p,T,j))) = (card (Support p)) - ((card (Support p)) - 1) by A1, A2, Th24;

then consider x being object such that

A3: Support (Low (p,T,j)) = {x} by CARD_2:42;

x in Support (Low (p,T,j)) by A3, TARSKI:def 1;

then A4: x is Element of Bags n ;

Low (p,T,j) <> 0_ (n,L) by A3, POLYNOM7:1;

hence Low (p,T,j) is non-zero Monomial of n,L by A3, A4, POLYNOM7:6, POLYNOM7:def 1; :: thesis: verum

for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr

for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L

for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let p be Polynomial of n,L; :: thesis: for j being Element of NAT st j = (card (Support p)) - 1 holds

Low (p,T,j) is non-zero Monomial of n,L

let j be Element of NAT ; :: thesis: ( j = (card (Support p)) - 1 implies Low (p,T,j) is non-zero Monomial of n,L )

set l = Low (p,T,j);

assume A1: j = (card (Support p)) - 1 ; :: thesis: Low (p,T,j) is non-zero Monomial of n,L

A2: now :: thesis: not j > card (Support p)

then
Support (Low (p,T,j)) = Lower_Support (p,T,j)
by Lm3;assume
j > card (Support p)
; :: thesis: contradiction

then ((card (Support p)) - 1) + 1 > (card (Support p)) + 1 by A1, XREAL_1:8;

then (card (Support p)) + (- (card (Support p))) > ((card (Support p)) + 1) + (- (card (Support p))) by XREAL_1:8;

hence contradiction ; :: thesis: verum

end;then ((card (Support p)) - 1) + 1 > (card (Support p)) + 1 by A1, XREAL_1:8;

then (card (Support p)) + (- (card (Support p))) > ((card (Support p)) + 1) + (- (card (Support p))) by XREAL_1:8;

hence contradiction ; :: thesis: verum

then card (Support (Low (p,T,j))) = (card (Support p)) - ((card (Support p)) - 1) by A1, A2, Th24;

then consider x being object such that

A3: Support (Low (p,T,j)) = {x} by CARD_2:42;

x in Support (Low (p,T,j)) by A3, TARSKI:def 1;

then A4: x is Element of Bags n ;

Low (p,T,j) <> 0_ (n,L) by A3, POLYNOM7:1;

hence Low (p,T,j) is non-zero Monomial of n,L by A3, A4, POLYNOM7:6, POLYNOM7:def 1; :: thesis: verum