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 card (Support p) = 0 by NAT_1:14;
then Support p, 0 are_equipotent by CARD_1:def 5;
then Support p = {} by CARD_1:46;
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;
HM p,T <> 0_ n,L by POLYNOM7:def 2;
then A3: Support (HM p,T) <> {} by POLYNOM7:1;
HT p,T in {x} by A1, A2, Th30;
then A4: Support (Up p,T,1) = {(HT p,T)} by A2, TARSKI:def 1;
then A5: Support (Up p,T,1) = Support (HM p,T) by A3, TERMORD:21;
A6: dom (HM p,T) = Bags n by FUNCT_2:def 1
.= dom (Up p,T,1) by FUNCT_2:def 1 ;

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 x' = x as Element of Bags n ;

now

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

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

then x' = HT p,T by A4, A5, TARSKI:def 1;
hence (HM p,T) . x' = p . x' by TERMORD:18
.= (Up p,T,1) . x' by A5, A7, Th16 ;
:: thesis: verum

end;

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

hence (HM p,T) . x' = 0. L by POLYNOM1:def 9
.= (Up p,T,1) . x' by A5, A8, POLYNOM1:def 9 ;
:: thesis: verum

end;

end;

end;

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

end;

hence HM p,T = Up p,T,1 by A6, FUNCT_1:9; :: thesis: Low p,T,1 = Red p,T
then A9: (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 A9, 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