let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being non-zero Polynomial of n,L holds
( Up p,T,1 = HM p,T & Low p,T,1 = Red p,T )
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr
for p being non-zero Polynomial of n,L holds
( Up p,T,1 = HM p,T & Low p,T,1 = Red p,T )
let L be non trivial right_complementable Abelian add-associative right_zeroed doubleLoopStr ; :: thesis: for p being non-zero Polynomial of n,L holds
( Up p,T,1 = HM p,T & Low p,T,1 = Red p,T )
let p be non-zero Polynomial of n,L; :: thesis: ( Up p,T,1 = HM p,T & Low p,T,1 = Red p,T )
set u = Up p,T,1;
set l = Low p,T,1;

A1: now

assume card (Support p) < 1 ; :: thesis: contradiction
then Support p = {} by NAT_1:14;
then p = 0_ n,L by POLYNOM7:1;
hence contradiction by POLYNOM7:def 2; :: thesis: verum

end;

then Support (Up p,T,1) = Upper_Support p,T,1 by Lm3;
then card (Support (Up p,T,1)) = 1 by A1, Def2;
then consider x being set such that
A2: Support (Up p,T,1) = {x} by CARD_2:60;
HT p,T in {x} by A1, A2, Th30;
then A3: Support (Up p,T,1) = {(HT p,T)} by A2, TARSKI:def 1;
HM p,T <> 0_ n,L by POLYNOM7:def 2;
then Support (HM p,T) <> {} by POLYNOM7:1;
then A4: Support (Up p,T,1) = Support (HM p,T) by A3, TERMORD:21;

A5: now

let x be set ; :: thesis: ( x in dom (HM p,T) implies (HM p,T) . x = (Up p,T,1) . x )
assume x in dom (HM p,T) ; :: thesis: (HM p,T) . x = (Up p,T,1) . x
then reconsider x9 = x as Element of Bags n ;

now

per cases ( x in Support (HM p,T) or not x in Support (HM p,T) ) ;

case A6: x in Support (HM p,T) ; :: thesis: (HM p,T) . x9 = (Up p,T,1) . x9

then x9 = HT p,T by A3, A4, TARSKI:def 1;
hence (HM p,T) . x9 = p . x9 by TERMORD:18
.= (Up p,T,1) . x9 by A4, A6, Th16 ;
:: thesis: verum

end;

case A7: not x in Support (HM p,T) ; :: thesis: (HM p,T) . x9 = (Up p,T,1) . x9

hence (HM p,T) . x9 = 0. L by POLYNOM1:def 9
.= (Up p,T,1) . x9 by A4, A7, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

hence (HM p,T) . x = (Up p,T,1) . x ; :: thesis: verum

end;

dom (HM p,T) = Bags n by FUNCT_2:def 1
.= dom (Up p,T,1) by FUNCT_2:def 1 ;
hence HM p,T = Up p,T,1 by A5, FUNCT_1:9; :: thesis: Low p,T,1 = Red p,T
then A8: (HM p,T) + (Low p,T,1) = p by A1, Th33;
thus Red p,T = p - (HM p,T) by TERMORD:def 9
.= ((Low p,T,1) + (HM p,T)) + (- (HM p,T)) by A8, POLYNOM1:def 23
.= (Low p,T,1) + ((HM p,T) + (- (HM p,T))) by POLYNOM1:80
.= (Low p,T,1) + (0_ n,L) by POLYRED:3
.= Low p,T,1 by POLYRED:2 ; :: thesis: verum