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 () 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 () 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 () 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 () 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 () holds
Low ((m *' p),T,i) = m *' (Low (p,T,i))

let i be Element of NAT ; :: thesis: ( i <= card () 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 () ; :: 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 ;
A12: term m = s by ;
then (m *' p) . u9 = (m . (term m)) * (p . t) by
.= (m . (term m)) * ((Low (p,T,i)) . t) by ;
then (m *' p) . u9 <> 0. L by ;
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 ;
then A15: s + t9 < s + t,T by ;
not t <= t9,T by ;
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 ;
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 ;
A25: term m = s by ;
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 ;
then (m *' (Low (p,T,i))) . u9 <> 0. L by ;
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 ;
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 ;
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 ;
then A35: term m = s by ;
hence (m *' (Low (p,T,i))) . b = (m . (term m)) * ((Low (p,T,i)) . t) by
.= (m . (term m)) * (p . t) by
.= (m *' p) . b by
.= (Low ((m *' p),T,i)) . b by ;
:: 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 ;
:: 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 ; :: thesis: verum