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 :: thesis: not Support p <> {}

assume Support p <> {} ; :: thesis: contradiction
then reconsider sp = Support p as non empty set ;
set u = the Element of sp;
the Element of sp in Support p ;
then reconsider u9 = the Element of sp 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 4;
b + u9 is Element of Bags n by PRE_POLY:def 12;
hence contradiction by A1, A2, POLYNOM1:def 4; :: thesis: verum

end;

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

end;

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

now :: thesis: not Support p = {}

reconsider sp = Support (b *' p) as non empty set by A3;
set u = the Element of sp;
the Element of sp in Support (b *' p) ;
then reconsider u9 = the Element of sp 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 4;
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 4; :: 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 4;

A8: now :: thesis: for b9 being bag of n st b9 in Support (b *' p) holds
b9 <= b + (HT (p,T)),T

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 4;
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 4;
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 5;
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 4;
hence HT ((b *' p),T) = b + (HT (p,T)) by A8, TERMORD:def 6; :: thesis: verum

end;

end;