let n be Ordinal; :: thesis: for T being connected TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds p - (Red p,T) = HM p,T
let T be connected TermOrder of n; :: thesis: for L being non trivial right_complementable add-associative right_zeroed doubleLoopStr
for p being Polynomial of n,L holds p - (Red p,T) = HM p,T
let L be non trivial right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for p being Polynomial of n,L holds p - (Red p,T) = HM p,T
let p be Polynomial of n,L; :: thesis: p - (Red p,T) = HM p,T
thus p - (Red p,T) = ((HM p,T) + (Red p,T)) - (Red p,T) by TERMORD:38
.= ((HM p,T) + (Red p,T)) + (- (Red p,T)) by POLYNOM1:def 23
.= (HM p,T) + ((Red p,T) + (- (Red p,T))) by POLYNOM1:80
.= (HM p,T) + (0_ n,L) by POLYRED:3
.= HM p,T by POLYNOM1:82 ; :: thesis: verum