theorem Th19: :: POLYVIE1:19

for L being non empty left_zeroed add-associative doubleLoopStr
for B1, B2 being bag of the carrier of L
for E being the carrier of b₁ -valued FinSequence holds (B1 + B2) (++) E = (B1 (++) E) + (B2 (++) E)