:: deftheorem Def1 defines bag_extend HILBASIS:def 1 :
for n, k being Nat
for b being bag of n
for b₄ being Element of Bags (n + 1) holds
( b₄ = b bag_extend k iff ( b₄ | n = b & b₄ . n = k ) );