let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (HM p,T) + (Red p,T) = p
let O be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L holds (HM p,O) + (Red p,O) = p
let L be non trivial right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for p being Polynomial of n,L holds (HM p,O) + (Red p,O) = p
let p be Polynomial of n,L; :: thesis: (HM p,O) + (Red p,O) = p

A1: now

let x be set ; :: thesis: ( x in Bags n implies p . x = ((HM p,O) + (Red p,O)) . x )
assume x in Bags n ; :: thesis: p . x = ((HM p,O) + (Red p,O)) . x
then reconsider x9 = x as Element of Bags n ;

now

per cases ( x = HT p,O or x <> HT p,O ) ;

case A2: x = HT p,O ; :: thesis: ((HM p,O) + (Red p,O)) . x = p . x

hence ((HM p,O) + (Red p,O)) . x = ((HM p,O) . (HT p,O)) + ((Red p,O) . (HT p,O)) by POLYNOM1:def 21
.= ((HM p,O) . (HT p,O)) + (0. L) by Lm18
.= (HM p,O) . (HT p,O) by RLVECT_1:10
.= p . x by A2, Lm8 ;
:: thesis: verum

end;

case A3: x <> HT p,O ; :: thesis: p . x = ((HM p,O) + (Red p,O)) . x

((HM p,O) + (Red p,O)) . x9 = ((HM p,O) . x9) + ((Red p,O) . x9) by POLYNOM1:def 21
.= ((HM p,O) . x9) + (p . x9) by A3, Lm19
.= (0. L) + (p . x9) by A3, Th19
.= p . x9 by RLVECT_1:10 ;
hence p . x = ((HM p,O) + (Red p,O)) . x ; :: thesis: verum

end;

end;

end;

hence p . x = ((HM p,O) + (Red p,O)) . x ; :: thesis: verum

end;

( dom p = Bags n & dom ((HM p,O) + (Red p,O)) = Bags n ) by FUNCT_2:def 1;
hence (HM p,O) + (Red p,O) = p by A1, FUNCT_1:9; :: thesis: verum