theorem :: POLYVIE1:21

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