let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L holds Red (p,T) < p,T
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being non-zero Polynomial of n,L holds Red (p,T) < p,T
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being non-zero Polynomial of n,L holds Red (p,T) < p,T
let p be non-zero Polynomial of n,L; :: thesis: Red (p,T) < p,T
(Red (p,T)) . (HT (p,T)) = 0. L by TERMORD:39;
then A1: not HT (p,T) in Support (Red (p,T)) by POLYNOM1:def 4;
p <> 0_ (n,L) by POLYNOM7:def 1;
then Support p <> {} by POLYNOM7:1;
then A2: HT (p,T) in Support p by TERMORD:def 6;
Red (p,T) < HM (p,T),T by Th33;
then A3: Red (p,T) <= HM (p,T),T ;
HM (p,T) <= p,T by Th34;
then Red (p,T) <= p,T by A3, Th27;
hence Red (p,T) < p,T by A2, A1; :: thesis: verum