theorem Th52:
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 add-associative right_zeroed associative commutative doubleLoopStr for
p1,
p2 being
Polynomial of
n,
L st
HT (
p1,
T),
HT (
p2,
T)
are_disjoint holds
for
b1,
b2 being
bag of
n st
b1 in Support (Red (p1,T)) &
b2 in Support (Red (p2,T)) holds
not
(HT (p1,T)) + b2 = (HT (p2,T)) + b1