:: deftheorem Def7 defines mpu HILBASIS:def 7 :
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 ((n + 1),R)),(Polynom-Ring (Polynom-Ring (n,R))) holds
( b₃ = mpu (n,R) iff for p1 being Polynomial of (n + 1),R
for p2 being Polynomial of n,R
for p3 being Polynomial of (Polynom-Ring (n,R))
for i being Element of NAT
for b being bag of n st p3 = b₃ . p1 & p2 = p3 . i holds
p2 . b = p1 . (b bag_extend i) );