let n be Ordinal; :: thesis:
let T be connected admissible TermOrder of n; :: thesis:
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis:
let p be Polynomial of n,L; :: thesis:
let m be non-zero Monomial of n,L; :: thesis:
let i be Element of NAT ; :: thesis:
set l = Low p,T,i;
set lm = Low (m *' p),T,i;
assume A1: i <= card (Support p) ; :: thesis:
then A2: i <= card (Support (m *' p)) by Th10;
A3: Support (m *' (Low p,T,i)) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low p,T,i) ) } by TERMORD:30;

A4: now

m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A5: Support m = {(term m)} by POLYNOM7:7;
then term m in Support m by TARSKI:def 1;
then A6: m . (term m) <> 0. L by POLYNOM1:def 9;
let u be set ; :: thesis:
assume A7: u in Support (m *' (Low p,T,i)) ; :: thesis:
then reconsider u9 = u as Element of Bags n ;
u in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low p,T,i) ) } by A3, A7;
then consider s, t being Element of Bags n such that
A8: u9 = s + t and
A9: s in Support m and
A10: t in Support (Low p,T,i) ;
A11: (Low p,T,i) . t <> 0. L by A10, POLYNOM1:def 9;
A12: term m = s by A9, A5, TARSKI:def 1;
then (m *' p) . u9 = (m . (term m)) * (p . t) by A8, POLYRED:7
.= (m . (term m)) * ((Low p,T,i) . t) by A1, A10, Th31 ;
then (m *' p) . u9 <> 0. L by A11, A6, VECTSP_2:def 5;
then A13: u9 in Support (m *' p) by POLYNOM1:def 9;

assume not s + t in Support (Low (m *' p),T,i) ; :: thesis:
then A14: s + t in Support (Up (m *' p),T,i) by A2, A8, A13, Th28;

let t9 be bag of n; :: thesis:
assume t9 in Support (Low p,T,i) ; :: thesis:
then s + t9 in Support (Low (m *' p),T,i) by A1, A12, Th40;
then A15: s + t9 < s + t,T by A2, A14, Th29;

assume t <= t9,T ; :: thesis:
then s + t <= s + t9,T by Th2;
hence contradiction by A15, TERMORD:5; :: thesis:

end;

hence t9 < t,T by TERMORD:5; :: thesis:

end;

then t < t,T by A10;
hence contradiction by TERMORD:def 3; :: thesis:

end;

hence u in Support (Low (m *' p),T,i) by A8; :: thesis:

end;

A16: Support (m *' p) c= { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by TERMORD:30;

let u be set ; :: thesis:
assume A17: u in Support (Low (m *' p),T,i) ; :: thesis:
then reconsider u9 = u as Element of Bags n ;
Support (Low (m *' p),T,i) c= Support (m *' p) by A2, Th26;
then u9 in Support (m *' p) by A17;
then A18: u9 in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support p ) } by A16;
m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A19: Support m = {(term m)} by POLYNOM7:7;
then term m in Support m by TARSKI:def 1;
then A20: m . (term m) <> 0. L by POLYNOM1:def 9;
consider s, t being Element of Bags n such that
A21: u = s + t and
A22: s in Support m and
A23: t in Support p by A18;
A24: p . t <> 0. L by A23, POLYNOM1:def 9;
A25: term m = s by A22, A19, TARSKI:def 1;
then A26: t in Support (Low p,T,i) by A1, A17, A21, Th40;
(m *' (Low p,T,i)) . ((term m) + t) = (m . (term m)) * ((Low p,T,i) . t) by POLYRED:7
.= (m . (term m)) * (p . t) by A1, A26, Th31 ;
then (m *' (Low p,T,i)) . u9 <> 0. L by A21, A20, A25, A24, VECTSP_2:def 5;
hence u in Support (m *' (Low p,T,i)) by POLYNOM1:def 9; :: thesis:

end;

then A27: Support (m *' (Low p,T,i)) = Support (Low (m *' p),T,i) by A4, TARSKI:2;

A28: now

let x be set ; :: thesis:
assume x in dom (m *' (Low p,T,i)) ; :: thesis:
then reconsider b = x as Element of Bags n ;

case A29: b in Support (m *' (Low p,T,i)) ; :: thesis:

then A30: b in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low p,T,i) ) } by A3;
A31: b in Support (Low (m *' p),T,i) by A4, A29;
consider s, t being Element of Bags n such that
A32: b = s + t and
A33: s in Support m and
A34: t in Support (Low p,T,i) by A30;
Support m = {(term m)} by A33, POLYNOM7:7;
then A35: term m = s by A33, TARSKI:def 1;
hence (m *' (Low p,T,i)) . b = (m . (term m)) * ((Low p,T,i) . t) by A32, POLYRED:7
.= (m . (term m)) * (p . t) by A1, A34, Th31
.= (m *' p) . b by A32, A35, POLYRED:7
.= (Low (m *' p),T,i) . b by A2, A31, Th31 ;
:: thesis:

end;

case A36: not b in Support (m *' (Low p,T,i)) ; :: thesis:

hence (m *' (Low p,T,i)) . b = 0. L by POLYNOM1:def 9
.= (Low (m *' p),T,i) . b by A27, A36, POLYNOM1:def 9 ;
:: thesis:

end;

end;

end;

hence (m *' (Low p,T,i)) . x = (Low (m *' p),T,i) . x ; :: thesis:

end;

dom (m *' (Low p,T,i)) = Bags n by FUNCT_2:def 1
.= dom (Low (m *' p),T,i) by FUNCT_2:def 1 ;
hence Low (m *' p),T,i = m *' (Low p,T,i) by A28, FUNCT_1:9; :: thesis: