:: deftheorem Def1 defines (++) POLYVIE1:def 1 :
for L being non empty doubleLoopStr
for B being bag of the carrier of L
for E being the carrier of b₁ -valued FinSequence
for b₄ being FinSequence of L holds
( b₄ = B (++) E iff ( len b₄ = len E & ( for n being Nat st 1 <= n & n <= len b₄ holds
b₄ . n = ((B * E) . n) * (E /. n) ) ) );