let n be Ordinal; :: thesis: for T being connected TermOrder of n
for p being Polynomial of n,L
for j being Element of NAT st j = (card ()) - 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 ()) - 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 ()) - 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 ()) - 1 holds
Low (p,T,j) is non-zero Monomial of n,L

let j be Element of NAT ; :: thesis: ( j = (card ()) - 1 implies Low (p,T,j) is non-zero Monomial of n,L )
set l = Low (p,T,j);
assume A1: j = (card ()) - 1 ; :: thesis: Low (p,T,j) is non-zero Monomial of n,L
A2: now :: thesis: not j > card ()
assume j > card () ; :: thesis: contradiction
then ((card ()) - 1) + 1 > (card ()) + 1 by ;
then (card ()) + (- (card ())) > ((card ()) + 1) + (- (card ())) by XREAL_1:8;
hence contradiction ; :: thesis: verum
end;
then Support (Low (p,T,j)) = Lower_Support (p,T,j) by Lm3;
then card (Support (Low (p,T,j))) = (card ()) - ((card ()) - 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 ;
then A4: x is Element of Bags n ;
Low (p,T,j) <> 0_ (n,L) by ;
hence Low (p,T,j) is non-zero Monomial of n,L by ; :: thesis: verum