theorem Th20: :: POLYVIE1:20

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