theorem Th43: :: GROEB_3:43

for n being Ordinal
for T being connected admissible TermOrder of n
for L being non trivial right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of n,L
for i being Element of NAT st i < card (Support p) holds
Low (p,T,(i + 1)) = Red ((Low (p,T,i)),T)