let L be non empty left_zeroed add-associative doubleLoopStr ; :: thesis: for B1, B2 being bag of the carrier of L
for E, F being the carrier of L -valued FinSequence holds (B1 + B2) (++) (E ^ F) = ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F))
let B1, B2 be bag of the carrier of L; :: thesis: for E, F being the carrier of L -valued FinSequence holds (B1 + B2) (++) (E ^ F) = ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F))
let E, F be the carrier of L -valued FinSequence; :: thesis: (B1 + B2) (++) (E ^ F) = ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F))
thus (B1 + B2) (++) (E ^ F) = (B1 (++) (E ^ F)) + (B2 (++) (E ^ F)) by Th19
.= ((B1 (++) E) ^ (B1 (++) F)) + (B2 (++) (E ^ F)) by Th20
.= ((B1 (++) E) ^ (B1 (++) F)) + ((B2 (++) E) ^ (B2 (++) F)) by Th20 ; :: thesis: verum