theorem Th55:
for
n being
Ordinal for
T being
connected admissible TermOrder of
n for
L being non
trivial right_complementable almost_left_invertible well-unital distributive Abelian add-associative right_zeroed associative commutative doubleLoopStr for
p1,
p2 being
non-zero Polynomial of
n,
L st
HT (
p1,
T),
HT (
p2,
T)
are_disjoint &
Red (
p1,
T) is
non-zero &
Red (
p2,
T) is
non-zero holds
PolyRedRel (
{p1},
T)
reduces ((HM (p2,T)) *' (Red (p1,T))) - ((HM (p1,T)) *' (Red (p2,T))),
p2 *' (Red (p1,T))