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 7
.= (HM (p,T)) + ((Red (p,T)) + (- (Red (p,T)))) by POLYNOM1:21
.= (HM (p,T)) + (0_ (n,L)) by POLYRED:3
.= HM (p,T) by POLYNOM1:23 ; :: thesis: verum