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

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

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 Support (Low (p,T,j)) = Lower_Support (p,T,j) by Lm3;
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