theorem Th54: :: GROEB_3:54

for n being Ordinal
for T being connected 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 Polynomial of n,L st HT (p1,T), HT (p2,T) are_disjoint holds
S-Poly (p1,p2,T) = ((Red (p1,T)) *' p2) - ((Red (p2,T)) *' p1)