let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L
for b being bag of n holds HT (b *' p),T = b + (HT p,T)
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial ZeroStr
for p being non-zero Polynomial of n,L
for b being bag of n holds HT (b *' p),T = b + (HT p,T)
let L be non trivial ZeroStr ; :: thesis: for p being non-zero Polynomial of n,L
for b being bag of n holds HT (b *' p),T = b + (HT p,T)
let p be non-zero Polynomial of n,L; :: thesis: for b being bag of n holds HT (b *' p),T = b + (HT p,T)
let b be bag of n; :: thesis: HT (b *' p),T = b + (HT p,T)
set htp = HT p,T;

per cases ( Support (b *' p) = {} or Support (b *' p) <> {} ) ;

suppose A1: Support (b *' p) = {} ; :: thesis: HT (b *' p),T = b + (HT p,T)

now

assume Support p <> {} ; :: thesis: contradiction
then reconsider sp = Support p as non empty set ;
consider u being Element of sp;
u in Support p ;
then reconsider u9 = u as Element of Bags n ;
b divides b + u9 by PRE_POLY:50;
then (b *' p) . (b + u9) = p . ((b + u9) -' b) by Def1
.= p . u9 by PRE_POLY:48 ;
then A2: (b *' p) . (b + u9) <> 0. L by POLYNOM1:def 9;
b + u9 is Element of Bags n by PRE_POLY:def 12;
hence contradiction by A1, A2, POLYNOM1:def 9; :: thesis: verum

end;

then p = 0_ n,L by POLYNOM7:1;
hence HT (b *' p),T = b + (HT p,T) by POLYNOM7:def 2; :: thesis: verum

end;

suppose A3: Support (b *' p) <> {} ; :: thesis: HT (b *' p),T = b + (HT p,T)

now

reconsider sp = Support (b *' p) as non empty set by A3;
consider u being Element of sp;
u in Support (b *' p) ;
then reconsider u9 = u as Element of Bags n ;
A4: u9 -' b is Element of Bags n by PRE_POLY:def 12;
A5: (b *' p) . u9 <> 0. L by POLYNOM1:def 9;
then b divides u9 by Def1;
then A6: p . (u9 -' b) <> 0. L by A5, Def1;
assume Support p = {} ; :: thesis: contradiction
hence contradiction by A6, A4, POLYNOM1:def 9; :: thesis: verum

end;

then HT p,T in Support p by TERMORD:def 6;
then A7: p . (HT p,T) <> 0. L by POLYNOM1:def 9;

A8: now

let b9 be bag of n; :: thesis: ( b9 in Support (b *' p) implies b9 <= b + (HT p,T),T )
assume b9 in Support (b *' p) ; :: thesis: b9 <= b + (HT p,T),T
then A9: (b *' p) . b9 <> 0. L by POLYNOM1:def 9;
then b divides b9 by Def1;
then consider b3 being bag of n such that
A10: b + b3 = b9 by TERMORD:1;
A11: b3 is Element of Bags n by PRE_POLY:def 12;
(b *' p) . b9 = p . b3 by A10, Lm9;
then b3 in Support p by A9, A11, POLYNOM1:def 9;
then b3 <= HT p,T,T by TERMORD:def 6;
then [b3,(HT p,T)] in T by TERMORD:def 2;
then [b9,(b + (HT p,T))] in T by A10, BAGORDER:def 7;
hence b9 <= b + (HT p,T),T by TERMORD:def 2; :: thesis: verum

end;

( (b *' p) . (b + (HT p,T)) = p . (HT p,T) & b + (HT p,T) is Element of Bags n ) by Lm9, PRE_POLY:def 12;
then b + (HT p,T) in Support (b *' p) by A7, POLYNOM1:def 9;
hence HT (b *' p),T = b + (HT p,T) by A8, TERMORD:def 6; :: thesis: verum

end;

end;