let n be Ordinal; :: thesis: for T being connected admissible TermOrder of n
for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
let T be connected admissible TermOrder of n; :: thesis: for L being non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
let L be non trivial right_complementable well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr ; :: thesis: for p being Polynomial of n,L
for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
let p be Polynomial of n,L; :: thesis: for m being non-zero Monomial of n,L
for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
let m be non-zero Monomial of n,L; :: thesis: for i being Element of NAT st i <= card (Support p) holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))
let i be Element of NAT ; :: thesis: ( i <= card (Support p) implies Low ((m *' p),T,i) = m *' (Low (p,T,i)) )
set l = Low (p,T,i);
set lm = Low ((m *' p),T,i);
assume A1: i <= card (Support p) ; :: thesis: Low ((m *' p),T,i) = m *' (Low (p,T,i))
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 :: thesis: for u being object st u in Support (m *' (Low (p,T,i))) holds
u in Support (Low ((m *' p),T,i))

m <> 0_ (n,L) by POLYNOM7:def 1;
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 4;
let u be object ; :: thesis: ( u in Support (m *' (Low (p,T,i))) implies u in Support (Low ((m *' p),T,i)) )
assume A7: u in Support (m *' (Low (p,T,i))) ; :: thesis: u in Support (Low ((m *' p),T,i))
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 4;
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 1;
then A13: u9 in Support (m *' p) by POLYNOM1:def 4;

now :: thesis: s + t in Support (Low ((m *' p),T,i))

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

now :: thesis: for t9 being bag of n st t9 in Support (Low (p,T,i)) holds
t9 < t,T

let t9 be bag of n; :: thesis: ( t9 in Support (Low (p,T,i)) implies t9 < t,T )
assume t9 in Support (Low (p,T,i)) ; :: thesis: t9 < t,T
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;
not t <= t9,T by A15, TERMORD:5, Th2;
hence t9 < t,T by TERMORD:5; :: thesis: verum

end;

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

end;

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

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;

now :: thesis: for u being object st u in Support (Low ((m *' p),T,i)) holds
u in Support (m *' (Low (p,T,i)))

let u be object ; :: thesis: ( u in Support (Low ((m *' p),T,i)) implies u in Support (m *' (Low (p,T,i))) )
assume A17: u in Support (Low ((m *' p),T,i)) ; :: thesis: u in Support (m *' (Low (p,T,i)))
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 1;
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 4;
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 4;
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 1;
hence u in Support (m *' (Low (p,T,i))) by POLYNOM1:def 4; :: thesis: verum

end;

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

A28: now :: thesis: for x being object st x in dom (m *' (Low (p,T,i))) holds
(m *' (Low (p,T,i))) . x = (Low ((m *' p),T,i)) . x

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

now :: thesis: ( ( b in Support (m *' (Low (p,T,i))) & (m *' (Low (p,T,i))) . b = (Low ((m *' p),T,i)) . b ) or ( not b in Support (m *' (Low (p,T,i))) & (m *' (Low (p,T,i))) . b = (Low ((m *' p),T,i)) . b ) )

per cases ( b in Support (m *' (Low (p,T,i))) or not b in Support (m *' (Low (p,T,i))) ) ;

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

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: verum

end;

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

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

end;

end;

end;

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

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:2; :: thesis: verum