:: deftheorem Def1 defines +^ POLYNOM6:def 1 :
for o1, o2 being Ordinal
for a being Element of Bags o1
for b being Element of Bags o2
for b₅ being Element of Bags (o1 +^ o2) holds
( b₅ = a +^ b iff for o being Ordinal holds
( ( o in o1 implies b₅ . o = a . o ) & ( o in (o1 +^ o2) \ o1 implies b₅ . o = b . (o -^ o1) ) ) );