:: deftheorem Def1 defines |. HILB10_5:def 1 :
for n being set
for p, b₃ being Series of n,F_Real holds
( b₃ = |.p.| iff for b being bag of n holds b₃ . b = |.(p . b).| );