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 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 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 holds HT (b *' p),T = b + (HT p,T)
let p be non-zero Polynomial of n,L; :: thesis: for b being bag of holds HT (b *' p),T = b + (HT p,T)
let b be bag of ; :: 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 u' = u as Element of Bags n ;
b divides b + u' by POLYNOM1:54;
then (b *' p) . (b + u') = p . ((b + u') -' b) by Def1
.= p . u' by POLYNOM1:52 ;
then A2: (b *' p) . (b + u') <> 0. L by POLYNOM1:def 9;
b + u' is Element of Bags n by POLYNOM1:def 14;
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

assume A4: Support p = {} ; :: thesis: contradiction
reconsider sp = Support (b *' p) as non empty set by A3;
consider u being Element of sp;
u in Support (b *' p) ;
then reconsider u' = u as Element of Bags n ;
A5: (b *' p) . u' <> 0. L by POLYNOM1:def 9;
then b divides u' by Def1;
then A6: p . (u' -' b) <> 0. L by A5, Def1;
u' -' b is Element of Bags n by POLYNOM1:def 14;
hence contradiction by A4, A6, 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: (b *' p) . (b + (HT p,T)) = p . (HT p,T) by Lm9;
b + (HT p,T) is Element of Bags n by POLYNOM1:def 14;
then A9: b + (HT p,T) in Support (b *' p) by A7, A8, POLYNOM1:def 9;

now

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

end;

hence HT (b *' p),T = b + (HT p,T) by A9, TERMORD:def 6; :: thesis: verum

end;

end;