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

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