theorem Th15: :: GROEB_3:15

for n being Ordinal
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)