:: deftheorem Def3 defines extended_by_0 HILB10_2:def 3 :
for n being Nat
for L being non empty ZeroStr
for p being Series of n,L
for b₄ being Series of (n + 1),L holds
( b₄ = p extended_by_0 iff for b being bag of n + 1 holds
( ( b . n <> 0 implies b₄ . b = 0. L ) & ( b . n = 0 implies b₄ . b = p . ((0,n) -cut b) ) ) );