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 )
assume A1: j = (card (Support p)) - 1 ; :: thesis: Low p,T,j is non-zero Monomial of n,L
set l = Low p,T,j;

A2: now

assume j > card (Support p) ; :: thesis: contradiction
then ((card (Support p)) - 1) + 1 > (card (Support p)) + 1 by A1, XREAL_1:10;
then (card (Support p)) + (- (card (Support p))) > ((card (Support p)) + 1) + (- (card (Support p))) by XREAL_1:10;
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 set such that
A3: Support (Low p,T,j) = {x} by CARD_2:60;
A4: Low p,T,j <> 0_ n,L by A3, POLYNOM7:1;
x in Support (Low p,T,j) by A3, TARSKI:def 1;
then x is Element of Bags n ;
hence Low p,T,j is non-zero Monomial of n,L by A3, A4, POLYNOM7:6, POLYNOM7:def 2; :: thesis: verum