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 :: thesis: for x being object st x in Bags n holds
p . x = ((HM (p,O)) + (Red (p,O))) . x

let x be object ; :: 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 :: thesis: ( ( x = HT (p,O) & ((HM (p,O)) + (Red (p,O))) . x = p . x ) or ( x <> HT (p,O) & p . x = ((HM (p,O)) + (Red (p,O))) . x ) )

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:15
.= ((HM (p,O)) . (HT (p,O))) + (0. L) by Lm18
.= (HM (p,O)) . (HT (p,O)) by RLVECT_1:4
.= 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:15
.= ((HM (p,O)) . x9) + (p . x9) by A3, Lm19
.= (0. L) + (p . x9) by A3, Th19
.= p . x9 by RLVECT_1:4 ;
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:2; :: thesis: verum