:: deftheorem Def2 defines Compress POLYNOM6:def 2 :
for o1, o2 being non empty Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for P being Polynomial of o1,(Polynom-Ring (o2,L))
for b₅ being Polynomial of (o1 +^ o2),L holds
( b₅ = Compress P iff for b being Element of Bags (o1 +^ o2) ex b1 being Element of Bags o1 ex b2 being Element of Bags o2 ex Q1 being Polynomial of o2,L st
( Q1 = P . b1 & b = b1 +^ b2 & b₅ . b = Q1 . b2 ) );