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 1; :: 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:42;
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 1;
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 3
.= (Up (p,T,1)) . x9 by A4, A7, POLYNOM1:def 3 ;
:: 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:2; :: 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 6
.= (Low (p,T,1)) + ((HM (p,T)) + (- (HM (p,T)))) by POLYNOM1:21
.= (Low (p,T,1)) + (0_ (n,L)) by POLYRED:3
.= Low (p,T,1) by POLYRED:2 ; :: thesis: verum