:: deftheorem Def6 defines upm HILBASIS:def 6 :
for R being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for n being Nat
for b₃ being Function of (Polynom-Ring (Polynom-Ring (n,R))),(Polynom-Ring ((n + 1),R)) holds
( b₃ = upm (n,R) iff for p1 being Polynomial of (Polynom-Ring (n,R))
for p2 being Polynomial of n,R
for p3 being Polynomial of (n + 1),R
for b being bag of n + 1 st p3 = b₃ . p1 & p2 = p1 . (b . n) holds
p3 . b = p2 . (b | n) );