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:
assume A1: i <= card (Support p) ; :: thesis:
then A2: i <= card (Support (m *' p)) by Th10;
set l = Low p,T,i;
set lm = Low (m *' p),T,i;
A3: dom (m *' (Low p,T,i)) = Bags n by FUNCT_2:def 1
.= dom (Low (m *' p),T,i) by FUNCT_2:def 1 ;
A4: 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;
A5: 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;

A6: now

let u be set ; :: thesis:
assume A7: u in Support (m *' (Low p,T,i)) ; :: thesis:
then reconsider u' = 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 A4, A7;
then consider s, t being Element of Bags n such that
A8: ( u' = s + t & s in Support m & t in Support (Low p,T,i) ) ;
A9: (Low p,T,i) . t <> 0. L by A8, POLYNOM1:def 9;
m <> 0_ n,L by POLYNOM7:def 2;
then Support m <> {} by POLYNOM7:1;
then A10: Support m = {(term m)} by POLYNOM7:7;
then term m in Support m by TARSKI:def 1;
then A11: m . (term m) <> 0. L by POLYNOM1:def 9;
A12: term m = s by A8, A10, TARSKI:def 1;
then (m *' p) . u' = (m . (term m)) * (p . t) by A8, POLYRED:7
.= (m . (term m)) * ((Low p,T,i) . t) by A1, A8, Th31 ;
then (m *' p) . u' <> 0. L by A9, A11, VECTSP_2:def 5;
then A13: u' 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 t' be bag of ; :: thesis:
assume t' in Support (Low p,T,i) ; :: thesis:
then s + t' in Support (Low (m *' p),T,i) by A1, A12, Th40;
then A15: s + t' < s + t,T by A2, A14, Th29;

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

end;

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

end;

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

end;

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

end;

now

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

end;

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

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

per cases ;

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

then A25: b in Support (Low (m *' p),T,i) by A6;
b in { (s + t) where s, t is Element of Bags n : ( s in Support m & t in Support (Low p,T,i) ) } by A4, A24;
then consider s, t being Element of Bags n such that
A26: ( b = s + t & s in Support m & t in Support (Low p,T,i) ) ;
Support m = {(term m)} by A26, POLYNOM7:7;
then A27: term m = s by A26, TARSKI:def 1;
hence (m *' (Low p,T,i)) . b = (m . (term m)) * ((Low p,T,i) . t) by A26, POLYRED:7
.= (m . (term m)) * (p . t) by A1, A26, Th31
.= (m *' p) . b by A26, A27, POLYRED:7
.= (Low (m *' p),T,i) . b by A2, A25, Th31 ;
:: thesis:

end;

case A28: 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 A23, A28, POLYNOM1:def 9 ;
:: thesis:

end;

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

end;

hence Low (m *' p),T,i = m *' (Low p,T,i) by A3, FUNCT_1:9; :: thesis: